Zur Seitennavigation oder mit Tastenkombination für den accesskey-Taste und Taste 1 
Zum Seiteninhalt oder mit Tastenkombination für den accesskey und Taste 2 
QIS-Portal vom * 11. - 15.11.2019 * nicht verfügbar! Weitere Informationen unter: https://www.tu-bs.de/it/aktuelles
Startseite    Anmelden    Semester: WiSe 2019/20      Switch to english language    Hilfe    Sitemap
Logout in [min] [minutetext]

Nebenläufigkeitstheorie - Einzelansicht

  • Funktionen:
Grunddaten
Veranstaltungsart Übung Langtext
Veranstaltungsnummer 4212060 Kurztext
Semester WiSe 2017/18 SWS 2.0
Erwartete Teilnehmer/-innen 30 Max. Teilnehmer/-innen 30
Rhythmus keine Übernahme Studienjahr
Credits Belegung Keine Belegpflicht
Hyperlink  
Sprache deutsch
Termine iCalendar Export für Outlook
  Tag Zeit Rhythmus Dauer Raum Raum-
plan
Lehrperson Status fällt aus am Max. Teilnehmer/-innen
Einzeltermine anzeigen
iCalendar Export für Outlook
Mi. 16:45 bis 18:15 woch Rebenring 58 - 58 b (3206) - 3206.01.103 - RR 58.4 (Seminarraum)       30
 
Zuordnung zu Einrichtungen
Institut für Theoretische Informatik
Inhalt
Kommentar QUALIFIKATIONSZIELE:
Die Studierenden entwickeln operationelle Modelle für Systeme aus interagierenden Komponenten. Sie kennen verschiedene Korrektheitsbegriffe und verstehen die zugehörigen Verifikationsalgorithmen. Sie sind in der Lage, analoge Verfahren für verwandte Systemmodelle zu entwerfen.

INHALTE:
Petri-Netze
===========
Petri-Netze als Modell der Nebenläufigkeit
Invarianten, die Marking-Equation
Überdeckbarkeit, Sätze von Lipton & Rackoff, Karp & Miller-Überdeckbarkeitsgraphen
Erreichbarkeit
Unfoldings
Eingeschränkte & erweiterte Varianten von Petri-Netzen
Petri-Netz-Sprachen

Wohlstrukturierte Transitionssysteme (WSTS)
===========================================
Wohlquasiordnungen, Aufwärts- & Abwärtsabschlüsse
Abdullas Rückwärtssuche
Geeraerts EEC-Algorithmus
Finkels Erreichbarkeitsbaum
Grenzwerte, Vorwärtsüberdeckbarkeit
Lossy-Channels-Systeme (LCS)
IC3 & IIC

Automatenmodelle für Nebenläufige Systeme
=========================================
Automaten mit verteiltem Alphabet
Multi-Pushdown-Systeme
Bounded-Context-Switching
Sequentialisierung

Schwache Speichermodelle
========================
Sequentielle Konsistenz
TSO, PSO, Power, C11
Erreichbarkeit unter schwachen Speichermodellen
Robustheit
Dataraces und DRF-Theoreme

Rekonfigurierbare Netzwerke und Prozessalgebra
==============================================
Calculus of Communicating Systems (CCS)
Bisimulationen
Pi-Kalkül
Tiefen- und Breitenbeschränktheit
Literatur L. Priese and H. Wimmel. Petri-Netze. Springer, 2003.

W. Reisig. Petri nets: An Introduction. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 1985.

P. H. Starke. Analyse von Petri-Netz-Modellen. Leitfäden und Monographien der Informatik. Teubner, 1990.

J. Esparza and S. Melzer. Verification of Safety Properties Using Integer Programming: Beyond the State Equation. Formal Methods in System Design, 2000.

J. Esparza. Decidability and complexity of Petri net problems ? an introduction. Lectures on Petri Nets I: Basic Models. Springer, 1998.

J. Esparza and M. Nielsen. Decibility issues for Petri nets-a survey. Journal of Information Processing and Cybernetics EIK, 30(3):143-160, 1994.

J. Esparza and K. Heljanko. Unfoldings. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2008.

C. Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science. Volume 6, issue 2, 1978.

C. Dufourd et al. Reset nets between decidability and undecidability. Automata, Languages and Programming, 1998.

P. Jan?ar. Undecidability of bisimilarity for Petri nets and some related problems. Theoretical Computer Science. Volume 148, issue 2, 1995.

P. Jan?ar, J. Esparza, and F. Moller, Petri nets and regular processes. Journal of Computer and System Sciences. Volume 59, issue 3, 1999.

A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science. Volume 256, issue 1-2, 2001.

C. ST. J. A. Nash-Williams. On well-quasi-ordering finite trees. In Mathematical Proceedings of the Cambridge Philosophical Society. Cambridge Univsity Press, 1963.

P. A. Abdulla, A. Collomb-Annichini, A. Bouajjani, and B. Jonsson. Using forward reachability analysis for verification of lossy channel systems. Formal Methods in System Design. Volume 25, issue 1, 2004.

A. Finkel and Goubault-J. Larrecq. Forward analysis for WSTS, part I: Completions. 26th International Symposium on Theoretical Aspects of Computer Science, 2009.

G. Geeraerts, J.-F. Raskin, L. Van Begin. Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS. Journal of Computer and System Sciences, 72(1):180-203, 2005.

P. Abdulla, A. Bouajjani, B. Jonsson. On-the-Fly Analysis of Systems with Unbounded, Lossy Fifo Channels. In Proc. of the 10th International Conference on Computer Aided Verification, CAV, volume 1427 of LNCS, pages 305-318, Springer, 1998.

M. F. Atig, A. Bouajjani, S. Burckhardt, M. Musuvathi. On the Verification Problem for Weak Memory Models.

P. A. Abdulla, M. F. Atig, Y.-F. Chen, C. Leonardsson, A. Rezine. Counter-Example Guided Fence Insertion under Weak Memory Models.

M. F. Atig, A. Bouajjani, G. Parlato. Getting Rid of Store-Buffers in TSO Analysis.

R. Milner. Communicating and mobile systems: the pi-calculus. Cambridge University Press, 1999.

D. Sangiorgi, D. Walker. Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, 2001.

R. Meyer. On boundedness in depth in the ?-calculus. Fifth IFIP International Conference On Theoretical Computer Science, 2008.

R. Meyer. Structural Stationarity in the pi-Calculus. PhD thesis, Department of Computing Science, University of Oldenburg, 2008.

T. Wies, D. Zufferey, and T. Henzinger. Forward analysis of depth-bounded processes. FoSSaCS, 2010.

E. D'Osualdo, C.H.-L. Ong. On Hierarchical Communication Topologies in the pi-calculus. Programming Languages and Systems: ESOP, 2016.

M. Mukund. Automata on Distributed Alphabets. Modern Applications of Automata Theory, 2012.

P. Saivasan. Analysis of Automata-theoretic models of Concurrent Recursive Programs. PhD thesis, Chennai Mathematical Institute, 2016.
Bemerkung Deutsch, bei Bedarf Englisch
Server: LSF16 Impressum & Datenschutz