Third party funded individual grant
Acronym: COAX
Start date : 01.10.2014
End date : 31.07.2018
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.