| Koinduktion und Algebra in der Axiomatisierung von Systemäquivalenz Ein wichtiges Problem im Bereich der Spezifikation und Verifikation sowohl sequentieller als auch paralleler Programme ist die Prüfung von Programmäquivalenz. Während Programmäquivalenz im Allgemeinen unentscheidbar ist (z.B. für Turing-vollständige Sprachen), lässt sich Entscheidbarkeit für geeignet abstrahierte Ausdruckssprachen, die nur Teilaspekte des Programmverhaltens beschreiben, wieder herstellen. Ein klassisches Beispiel hierfür sind reguläre Ausdrücke, die lediglich den Kontrollfluss eines sequentiellen Programms beschreiben und deren Äquivalenz PSPACE-vollständig ist. Für Systeme mit endlichem Zustandsraum gibt es neuerdings generische Verfahren, die ein Ausdruckskalkül mit entscheidbarer Äquivalenz aus dem Systemtyp ableiten; diese liefern z.B. das o.g. Ergebnis für reguläre Sprachen als Spezialfall. Das Ziel von COAX ist die Entwicklung von Ausdruckssprachen, Beweiskalkülen und Algorithmen für die Äquivalenz von Systemen, deren Zustandsraum zwar unendlich, aber finitär ist, d.h. eine endliche algebraische Präsentation hat. Zum Beispiel ist der Zustandsraum eines gewichteten Automaten ein endlich dimensionaler Vektorraum über einem Körper; er ist somit im Allgemeinen unendlich, hat aber eine endliche Präsentation durch seine Basis. Wie schon o.g. Resultate über endliche Systeme werden unsere Arbeiten auf dem Prinzip der universellen Koalgebra basieren, die große Klassen zustandsbasierter Systeme, neben klassischen (nicht)deterministischen Automaten z.B. auch gewichtete, probabilistische und spieltheoretische Systeme, in einer vereinheitlichten Sicht behandelt. Die geplante Entwicklung kombiniert und erweitert verschiedene aktuelle Forschungsrichtungen: Turi und Plotkins mathematische operationelle Semantik; die von Rutten et al. initiierte koalgebraische Vereinheitlichung automatentheoretischer Konstruktionen; die von Pattinson und einem der Antragsteller (Schröder) entwickelte koalgebraische Logik der Prädikatenliftings; Silvas koalgebraische Ausdruckskalküle für Mengenfunktoren; und die von einem der Antragsstellers (Milius) und Koautoren eingeführte generische Semantik finitärer Systeme. Wir werden hierbei über allgemeinen algebraischen Kategorien arbeiten und somit über den bisher üblichen rein mengentheoretischen Ansatz hinausgehen. Damit erhalten wir generische Sprachen und koinduktive Methoden für automatische Äquivalenzbeweise über finitären Systemen mit entsprechend strukturierten Zustandsräumen. Diese generischen Resultate werden für wichtige konkrete Systemtypen instanziiert: arbeitet man z.B. über Halbverbänden, Moduln über Semiringen oder positiv konvexen Algebren, erhält man Verifikationsmethoden für verschiedene Typen nichtdeterministischer, gewichteter bzw. probabilistischer Systeme; über Prägarben oder nominalen Mengen erhält man Sprachen mit Bindungs- und Kommunikationsoperationen für Variablen bzw. Namen, bis hin zum pi-Kalkül. | Projektleitung:
Prof. Dr. Stefan Milius, Prof. Dr. Lutz Schröder
Beteiligte:
Ulrich Dorsch, Dr.-Ing. Thorsten Wißmann
Stichwörter:
Koalgebra; Ausdruckskalküle; Algebra; Äquivalenzprüfung
Laufzeit: 1.10.2014 - 31.5.2018
Förderer:
Deutsche Forschungsgemeinschaft
| | Publikationen |
|---|
Kurz, Alexander ; Milius, Stefan ; Pattinson, Dirk ; Schröder, Lutz: Simplified Coalgebraic Trace Equivalence. In: de Nicola, Rocco ; Hennicker, Rolf (Hrsg.) : Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering. Bd. 8950. Berlin : Springer, 2015, (Lecture Notes in Computer Science), S. 75-90. - ISBN 978-3-319-15544-9
[doi>10.1007/978-3-319-15545-6_8] | Myers, Robert S. L. ; Adámek, Jirí ; Milius, Stefan ; Urbat, Henning : Coalgebraic Constructions of Canonical Nondeterministic Automata. In: Theoretical Computer Science (2015), Nr. 604, S. 81-101
[doi>10.1016/j.tcs.2015.03.035] | Milius, Stefan ; Wißmann, Thorsten: Finitary Corecursion for the Infinitary Lambda Calculus. In: Moss, Lawrence S. ; Sobocinski, Pawel (Hrsg.) : Proc. 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015 (CALCO 2015 Nijmegen (NL) 24.-26.06.2015). Bd. 35. 2015, S. 336-351. (Leibniz International Proceedings in Informatics) - ISBN 978-3-939897-84-2
[doi>10.4230/LIPIcs.CALCO.2015.336] | Bonchi, Filippo ; Milius, Stefan ; Silva, Alexandra ; Zanasi, Fabio: Killing Epsilons with a Dagger: A Coalgebraic Study of Systems with Algebraic Label Structure. In: Theoretical Computer Science (2015), Nr. 604, S. 102-126
[doi>10.1016/j.tcs.2015.03.024] | Adamek, Jiri ; Urbat, Henning ; Milius, Stefan ; Moss, Lawrence S.: On Finitary Functors and Their Presentation. In: J. Comput. System Sci. 81 (2015), Nr. 5, S. 813-833
[doi>10.1016/j.jcss.2014.12.002] | Adámek, Jirí ; Milius, Stefan ; Urbat, Henning : Syntactic Monoids in a Category. In: Moss, Lawrence S. ; Sobocinski, Pawel (Hrsg.) : Coalgebraic and Algebraic Methods in Computer Science (CALCO'15) (6th Conference on Algebra and Coalgebra in Computer Science Nijmegen 24.-26.06.2015). Bd. 35. Schloss Dagstuhl : Leibniz-Zentrum fuer Informatik, 2015, S. 1-16. CALCO 2015 Best Paper. (LIPICS Bd. 35) - ISBN 978-3-939897-84-2
[doi>10.4230/LIPIcs.CALCO.2015.1] | Adámek, Jirí ; Milius, Stefan ; Myers, Robert S.R. ; Urbat, Henning: Varieties of Languages in a Category. In: Palamidessi, Catuscia (Hrsg.) : 30th Annual Symposium on Logic in Computer Science (LICS'15) (Thirtieth Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE Kyoto, Japan 06.-10.07.2015). 2015, S. 414-425. - ISBN 978-1-4799-8875-4
[doi>10.1109/LICS.2015.46] | Milius, Stefan ; Pattinson, Dirk ; Schröder, Lutz: Generic Trace Semantics and Graded Monads. In: Moss, Lawrence ; Sobocinski, Pawel (Hrsg.) : 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015 (6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015 Nijmegen June 24-26, 2015). Dagstuhl : Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015, S. 253-269. (LIPIcs Bd. 35) - ISBN 978-3-939897-84-2
[doi>10.4230/LIPIcs.CALCO.2015.253] | Milius, Stefan ; Litak, Tadeusz: Guard Your Daggers and Traces: Properties of Guarded (Co-)recursion. In: Fundamenta Informaticae (2017), Nr. 150, S. 407-449
[doi>10.3233/FI-2017-1475] | | Schröder, Lutz ; Kozen, Dexter ; Milius, Stefan ; Wißmann, Thorsten: Nominal Automata with Name Binding. In: Esparza, Javier ; Murawski, Andrzej (Hrsg.) : Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017)) (19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017)) Uppsala, Sweden 22-29.04.2017). Berlin : Springer, 2017, S. -. (Lecture Notes in Computer Science) | Milius, Stefan ; Pattinson, Dirk ; Wißmann, Thorsten: A New Foundation for Finitary Corecursion. In: Jacobs, Bart ; Löding, Christof (Hrsg.) : Foundations of Software Science and Computation Structures (19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) Eindhoven, The Netherlands 2.-8. April 2016). 2016, S. 107-125. (Lecture Notes in Computer Science Bd. 9634) - ISBN 978-3-662-49629-9
[doi>10.1007/978-3-662-49630-5] | Chen, Liang-Ting ; Adámek, Jirí ; Milius, Stefan ; Urbat, Henning : Profinite Monads, Profinite Equations and Reitermann's Theorem. In: Jacobs, Bart ; Löding, Christof (Hrsg.) : Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016 (19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) Eindhoven (The Netherlands) 02.-08.04.2016). Heidelberg : Springer, 2016, S. 531–547. (Lecture Notes in Computer Science Bd. 9634) - ISBN 978-3-662-49629-9
[doi>10.1007/978-3-662-49630-5_31] | Pattinson, Dirk ; Schröder, Lutz: Program equivalence is coinductive. In: Grohe, Martin ; Koskinen, Eric ; Shankar, Natarajan (Hrsg.) : Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 (31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 New York 05.-08.07.2016). New York : ACM, 2016, S. 337-346. - ISBN 978-1-4503-4391-6
[doi>10.1145/2933575.2934506] | Milius, Stefan ; Schröder, Lutz ; Wißmann, Thorsten: Regular Behaviours with Names - On Rational Fixpoints of Endofunctors on Nominal Sets. In: Applied Categorical Structures 5 (2016), Nr. 24, S. 663-791
[doi>10.1007/s10485-016-9457-8] |
|