Coinduction Meets Algebra For the Axiomatization of System Equivalence

Third party funded individual grant

Project Details

Project leader:
apl. Prof. Dr. Stefan Milius
Prof. Dr. Lutz Schröder

Project members:
Thorsten Wißmann
Ulrich Dorsch

Contributing FAU Organisations:
Lehrstuhl für Informatik 8 (Theoretische Informatik)

Funding source: DFG-Einzelförderung / Sachbeihilfe (EIN-SBH)
Acronym: COAX
Start date: 01/10/2014
End date: 31/07/2018

Abstract (technical / expert description):

An important task in the specification and verification of both sequential and concurrent programs is reasoning over program equivalence. While program equivalence is in general undecidable for full-blown (e.g. Turing complete) programming languages, it often stays decidable for suitably abstracted expression languages that capture only part of the program behaviour. A classical example are regular expressions, which reflect only the control flow of a (sequential) program, and whose equivalence problem is decidable, in fact PSPACE complete. For the case of finite-state systems, generic methods for designing expression languages and associated decision procedures are known; indeed decidability of regular language equivalence arises as one instance of these generic results. The goal of COAX is to develop generic languages, reasoning systems and algorithms for the specification and equivalence checking of systems whose state spaces are infinite but finitary, i.e. have a finite algebraic presentation. For example, the state space of a weighted automaton is a finite dimensional vector space over a given field; as such, it may be infinite but has a finite representation in terms of its basis.As in the finite-state case, we will base these developments on universal coalgebra, which provides a uniform view of a wide range of state-based systems including, besides classical deterministic or non-deterministic systems, e.g. weighted, probabilistic, and game-based systems. The planned work will combine and extend several recent strands of research including mathematical operational semantics as introduced by Turi and Plotkin; the coalgebraic uniformization of automata-theoretic constructions initiated by Rutten et al., as well as the coalgebraic logic of predicate liftings as developed by Pattinson and one of the applicants (Schröder); coalgebraic regular expression calculi for set functors as studied by Silva et al.; bisimulation up-to-techniques recently suggested by Bonchi and Pous; and a general theory of the behaviour of finitary systems developed by one of the applicants (Milius). Going beyond the set-theoretic set-up predominantly used in previous work, we will work over algebraic categories in a general sense, including for example the category of nominal sets, in order to obtain uniform and generic languages and coinductive methods for automated equivalence proofs for finitary systems with correspondingly structured state spaces. We will instantiate these results to several system types of interest -- e.g. working over join-semilattices, modules for semirings, and positive convex algebras, respectively, will yield verification methods for various types of non-deterministic, weighted, and probabilistic systems; and working over suitable presheaf categories or nominal sets will enable reasoning in languages with variable binding or name passing, up to and including the pi-calculus.

Go to first page Go to previous page 1 of 2 Go to next page Go to last page

Adámek, J., Milius, S., & Urbat, H. (2018). A Categorical Approach to Syntactic Monoids. Logical Methods in Computer Science, 14(2:9), 34 pp..
Adámek, J., Milius, S., & Moss, L. (2018). Fixed Points of Functors. Journal of Logical and Algebraic Methods in Programming, 95, 41--81.
Milius, S., Adámek, J., & Urbat, H. (2018). On Algebras with Effectful Iteration. In Corina Cîrstea (Eds.), Proc.~Coalgebraic Methods in Computer Science (CMCS'18). Thessaloniki: Heidelberg: Springer.
Dorsch, U., Milius, S., Schröder, L., & Wißmann, T. (2018). Predicate Liftings and Functor Presentations in Coalgebraic Expression Languages. In Corina Cîrstea (Eds.), Proc.~Coalgebraic Methods in Computer Science (CMCS'18). Thessaloniki: Springer.
Dorsch, U., Milius, S., Schröder, L., & Wißmann, T. (2017). Efficient Coalgebraic Partition Refinement. In Meyer R, Nestmann U (Eds.), Proc. 28th International Conference on Concurrency Theory (CONCUR 2017) (pp. 28:1--28:16). Schloss Dagstuhl.
Urbat, H., Adámek, J., Chen, L.-T., & Milius, S. (2017). Eilenberg Theorems for Free. In G.~Larsen K, L.~Bodlaender H, Raskin J (Eds.), Proc.~42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017) (pp. 43:1-43:14). Schloss Dagstuhl.
Milius, S., & Litak, T.M. (2017). Guard Your Daggers and Traces: Properties of Guarded (Co-)recursion. Fundamenta Informaticae, 150, 407-449.
Schröder, L., Kozen, D., Milius, S., & Wißmann, T. (2017). Nominal Automata with Name binding. In Esparza Javier, Murawski Andrzej (Eds.), Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017). Uppsala, SE: Springer.
Adámek, J., & Milius, S. (2017). On Corecursive Algebras for Functors Preserving Coproducts. In Bonchi F, König B (Eds.), Proc.~7th Conference on Algebra and Coalgebra in Computer Science (CALCO'17) (pp. 3:1--3:15). Schloss Dagstuhl.
Milius, S. (2017). Proper Functors and their Rational Fixed Point. In Bonchi F, König B (Eds.), Proc.~7th Conference on Algebra and Coalgebra in Computer Science (CALCO'17) (pp. 18:1--18:15). Schloss Dagstuhl.

Last updated on 2018-20-06 at 11:21