B-KUL-G0B23A Modellering van complexe systemen
Algemeen
-
Academiejaar: 2011-2012
-
Studiepunten: 6
-
Onderwijstaal: Nederlands
-
Niveau:
Verdiepend
-
Begeleidingsuren:
82.0 uren
-
Periode:
Wordt gedoceerd in het eerste semester
-
Verantwoordelijke POC:
POC Computerwetenschappen
|  Afdrukversie
|
Docenten/didactisch team
Denecker Marc
Doelstellingen
De student wordt vertrouwd gemaakt met een aantal basislogicas en formele technieken om een complex systeem te modelleren. Ze begrijpen voor welke types van proposities deze talen geschikt zijn en zijn in staat om relevante eigenschappen in deze talen uit te drukken en om hiermee bepaalde types van taken of problemen, inclusief verificatietaken mee op te lossen door middel van de geschikte inferentie. De keuze voor het gebruik van een bepaalde taal of inferentietechniek moet kunnen verantwoord worden. Globale voor- en nadelen van de technieken moeten gekend zijn en gebruikt worden bij die keuze, en de verbanden en verschillen tussen deze talen moeten gekend zijn.
Studenten zijn in staat de relevante concepten voor een probleemstelling in een domein te onderscheiden en er een ontologie of logisch vocabularium voor te ontwerpen. Ze zijn in staat naast expliciet gegeven informatie ook impliciete informatie te onderkennen in een probleemstelling. Ze kunnen beide types van informatie expliciteren in de logicas van deze cursus, of beoordelen in hoeverre deze geschikt zijn hiervoor. Ze kunnen een klasse van problemen of taken classifieren als logische formele inferentietaken, en zijn in staat om deze concreet te specifieren en te laten uitvoeren door het geschikte inferentietool.
De studenten zijn vertrouwd met een aantal informatieconcepten zoals unique names proposities, domain closure proposities, enumeratie, voldoende en noodzakelijke voorwaarden, inductieve definities, inertie in dynamische systemen, temporele eigenschappen in de context van dynamische systemen, en pre- en postcondities, Hoare triples, invarianten en varianten in de context van te verifieren programma's. Ze beheersen de modelleringstechnieken om deze proposities uit te drukken.
De studenten zijn vertrouwd met fundamentele theoretische concepten uit de logica zoals logische implicatie, satisfieerbaarheid, logische equivalentie, onvolledigheidsstelling van Goedel, bepaalde expressiviteitsbeperkingen en onbeslisbaarheid van logische implicatie voor klassieke logica en kunnen deze uitleggen. Van bepaalde basiseigenschappen kunnen ze het bewijs formuleren.
De studenten begrijpen een aantal fundamentele inferentiealgoritmes en kunnen deze beschrijven, inclusief de complexiteit ervan en ze handmatig illustreren voor kleine problemen.
Studenten zijn in staat partiele en volledige correctheid van programma's te bewijzen in Hoare logica.
De verschillende onderwerpen die aan bod komen tijdens de cursus en de gebruikte systemen sluiten dicht aan bij actueel onderzoek. In de cursus worden vele links gelegd tussen diverse onderzoeksgebieden in formele technieken en artificiële intelligentie en we stuiten geregeld op onopgeloste onderzoeksvragen.
Begintermen
Cursussen waarin de student heeft kennisgemaakt met propositionele logica, predicatenlogica, eindige automaten, programmeren, algorithmen, elementaire correctheidsbewijzen van programma’s. Aan de K.U.Leuven zijn deze cursussen concreet (zoals in de Bachelor Informatica): Logica voor Informatici, Beginselen van Programmeren, Fundamenten voor de Informatica, Object-gericht programmeren, Artificiele Intelligentie, Automaten en Berekenbaarheid.
Inhoud
De inhoud van het opleidingsonderdeel is gebaseerd op het boek Logic in Computer Science van Michael Huth and Mark Ryan. Het boek bevat vele oefeningen. De auteurs hebben een website met voor elk hoofdstuk een aantal meerkeuzevragen met feedback voor elke gemaakte keuze.
Het boek gaat dieper in op bepaalde onderwerpen dan de bedoeling is voor dit opleidingsonderdeel. In het bijzonder de secties over modale logica en OBDDs kunnen zonder probleem overgeslagen worden. Op andere vlakken gaat de cursus dan weer aanzienlijk dieper dan het boek. In het bijzonder gaan we veel dieper in op modellering en problem solving in klassieke logica. Ook worden veel meer verbanden gelegd tussen de verschillende hoofdstukken dan in het boek.
De cursus is onderverdeeld in de volgende hoofdstukken:
0. Inleiding
- Wat is modellering
- Een cursus op de confluentie van twee wetenschappelijke disciplines
- Over de rol van Kennisrepresentatie en formele methodes in computerwetenschappen
- Motivatie voor deze cursus
1. Propositionele logica als formele talen
- Syntax, semantiek
- Normalisatie
- SAT algoritmes
2. Predicatenlogica
- Syntax, semantiek
- Onbeslisbaarheid
- Uitdrukkingskracht
- Uitbreidingen van predicatenlogica
- Problem solving door middel van logische inferentie-systemen:
+ database model checking en query answering inferentie als model checking
+ modelgeneratie, modelrevisie
+ theorem proving/deductie
3. Modellering van dynamische systemen
- Het frame-probleem
- Een Lineaire Tijd Calculus (LTC) in predicatenlogica
- Verificatie, simulatie en planning voor dynamische systemen
4. Verificatie door modelchecking
- Motivatie voor verificatie
- Temporele logica's
* lineaire-tijd temporele logica’s (LTL): syntax, semantiek, specificatiepatronen, equivalenties, connectieven, links met Lineaire Tijd Calculus
* splitsende-tijd temporele logica (CTL): syntax, semantiek, specificatiepatronen, equivalenties, connectieven
* vergelijking van LTL en CTL
- Model checking
* modelchecking in LTL m.b.v. automaten
* modelchecking in CTL
* SAT-oplossers voor modelchecking
5. Programmaverificatie
- Een raamwerk voor softwareverificatie.
* core programmeertaal
* Hoare 3-tallen
* partiele en totale correctheid
- Bewijscalculus voor partiele correctheid
* bewijsregels en bewijstechniek
* toepassing
- Bewijscalculus voor totale correctheid
- Links met LTC en toepassing van logische inferentie voor programmaverificatie
Plaats in het onderwijsaanbod
Master of Science in de wiskunde
Master of Science in de toegepaste informatica
Master of Science in de ingenieurswetenschappen: computerwetenschappen (nieuw programma, start in 2010) (Verplicht)
Aard van het studiemateriaal
Handboek
Toledo
Onderwijsleeractiviteiten
 |
 |
B-KUL-G0B23a Modellering van complexe systemen |
| |
Algemeen
-
Studiepunten: 3.50
-
Onderwijstaal: Nederlands
-
Werkvorm:
Colleges
-
Begeleidingsuren:
26.0 uren
-
Periode:
Wordt gedoceerd in het eerste semester
-
Verantwoordelijke POC:
POC Computerwetenschappen
Docenten/didactisch team
Denecker Marc
Doelstellingen
De studenten moeten fundamenteel wetenschappelijke inzichten verwerven over formele talen en modellering bij te brengen (hoe werkt modellering, wat is het verband tussen modellering en semantiek van een taal, diverse types van taalconstructies, expressiviteit,..). Ze moeten verschillende modelleringsmethodologieen beheersen. Ze moeten ook de verbanden en verschillen tussen de verschillende formele talen begrijpen.
Ze moeten inzien hoe modelleringen gebruikt kunnen worden om diverse types van problemen op te lossen door middel van inferentie.
De studenten verwerven inzicht in state-of-the-art algoritmes van een paar belangrijke vormen van inferentie.
De studenten verwerven krijgen een overzicht van de stand van zaken en huidige evoluties van het gebruik van modelleringstechnieken in wetenschap en industrie.
Inhoud
De onderwerpen behandeld in de hoorcolleges werden beschreven het globale opleidingsonderdeel
G0B23A Modellering van complexe systemen.
Studiemateriaal
- Transparanten: zijn volledig en bevatten alle informatie die verondersteld wordt gekend te zijn op het examen.
- "Logic in Computer Science" van Michael Huth and Mark Ryan: wordt gebruikt als ondersteuning van de cursus. Er is een overlap van ongeveer 70%. Het boek wordt vooral nauw gevolgd in de hoofdstukken over modelchecking en Hoare logica.
- The transparanten, projectopgaves, oefeningen, huiswerken worden beschikbaar gesteld op Toledo.
- Eveneens op Toledo is er een forum voor de studenten waar ze kunnen discussieren over de cursus, de oefeningen, het project, de huiswerken.
Beschrijving leeractiviteit
De hoorcolleges zijn ex cathedra en gericht op kennisoverdracht. Dat is nodig omdat de
onderwerpen van de cursus totaal nieuw zijn voor de studenten en erg
verschillend van de onderwerpen in de meeste andere vakken in hun
opleiding. Een onderwijsvorm gebaseerd op bv. het lezen van artikels zou niet werken voor deze cursus. Het wetenschappelijk onderzoek is daarvoor veel te gefragmenteerd.
Er wordt veel aandacht gegegeven aan het leggen van verbanden
tussen de verschillende logicas en systemen die aan bod komen in de
verschillende hoofdstukken: bij probleemstellingen in latere hoofdstukken worden geevalueerd in hoeverre ze opgelost kunnen worden met technieken uit vroegere hoofdstukken. Enkel op deze manier kan een dieper inzicht in de
onderwerpen van de cursus bereikt worden. Het boek laat hier veel te wensen over.
De cursus is ook opgebouwd als een integratie van
twee
wetenschappelijke disciplines: kennisrepresentatie en formele methodes
en integreert inzichten en methodes uit beide wat eveneens de cursus
verrijkt in vergelijking met het boek van Huth en Ryan.
Door middel
van huiswerken - facultatieve opgaves in de transparanten, worden de
studenten aangemoedigd om dieper na te denken over de onderwerpen van de
cursus en om hun begrip te evalueren.
|
|
|
|
B-KUL-G0B24a Modellering van complexe systemen: Werkzittingen |
| |
Algemeen
-
Studiepunten: 1.50
-
Onderwijstaal: Nederlands
-
Werkvorm:
Oefenzittingen
-
Begeleidingsuren:
26.0 uren
-
Periode:
Wordt gedoceerd in het eerste semester
-
Verantwoordelijke POC:
POC Computerwetenschappen
Docenten/didactisch team
Denecker Marc
Doelstellingen
Doelstelling is het verwerven van practisch inzicht in de formele talen, de methodologieen voor het modelleren,
en de toepassing van diverse types van inferentiesystemen.
Inhoud
Tijdens de oefenzittingen wordt op alle onderdelen van de syllabus oefeningen gemaakt. Van de 10 sessies zijn de eerste en de laatste op papier: over het modelleren van domeinen in klassieke logica en bewijzen van correctheid van programma's met Hoare logica. Alle andere sessies zijn op computer en gaan over het modeleren van domeinen en systemen in diverse logica's en het gebruik van inferentiesystemen voor problem solving en verificatie.
Studiemateriaal
- Logic in Computer Science van Michael Huth and Mark Ryan
- Het IDP-systeem voor eindige modelgeneratie voor klassieke logica
- Het NuSMV-systeem voor model checking van CTL en LTL
Beschrijving leeractiviteit
Begeleide oefenzittingen
|
|
|
|
B-KUL-G0B25a Modellering van complexe systemen: Project |
| |
Algemeen
-
Studiepunten: 1.00
-
Onderwijstaal: Nederlands
-
Werkvorm:
Oefenzittingen
-
Begeleidingsuren:
30.0 uren
-
Periode:
Wordt gedoceerd in het eerste semester
-
Verantwoordelijke POC:
POC Computerwetenschappen
Docenten/didactisch team
Denecker Marc
Doelstellingen
Toepassen en inoefenen van het geleerde in de context
van een grotere oefening in modellering en het gebruik ervan voor verificatie.
Begrip van de verbanden en verschillen tussen de
twee belangrijkste modelleertechnieken en systemen
van deze cursus.
Inhoud
Het project is een groepswerk (2 personen) met als doel een dynamisch systeem te modelleren en te verifiëren in twee verschillende talen: de Linear Time Calculus en in NUSMV. Het project loopt van week 5 tot week
11.
Studenten die geen project indienen of gebuisd zijn voor het project moeten in de septemberzittijd een verbeterde versie van het project indienen.
Studiemateriaal
- IDP-systeem voor eindig modelgeneratie voor predicatenlogica
- NuSMV voor model checking voor temporele logica
Beschrijving leeractiviteit
In het project moet hetzelfde systemen met 2 verschillende manieren gemodelleerd en geverifieerd worden. Op die manieren worden de sterktes en zwaktes van beide formele talen duidelijk. De studenten moeten in hun verslag ook een evaluatie en vergelijking maken.
|
|
Evaluatieactiviteiten
|
|
B-KUL-G2B23a Evaluatie : Modellering van complexe systemen |
| |
Evaluatievorm
Modaliteit van de evaluatie:
mondeling met schriftelijke voorbereiding
Soort evaluatie:
Gesloten boek
Toelichting
Het examen bestaat uit een theoretisch mondeling gedeelte op 08/20 en een schriftelijk gedeelte op 7/20. Het project telt voor 5/20.
Indien het project niet ingediend wordt, krijgen de studenten 0/5 voor dit onderdeel, onafhankelijk of ze het examen afleggen in juni of september.
|
|
