LANGE , Martin

Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed λ-calculus into the modal µ-calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely...

International audience

Process equivalences are formal methods that relate programs and systems which, informally, behave in the same way. Since there is no unique notion of what it means for two dynamic systems to display the same behaviour there are a multitude of formal process equivalences, ranging from bisimulation to trace equivalence, categorised in the...

Multi-buffer simulation is a refinement of fair simulation between two nonde-terministic B ¨ uchi automata (NBA). It is characterised by a game in which letters get pushed to and taken from FIFO buffers of bounded or unbounded capacity. Games with a single buffer approximate the PSPACE-complete language inclusion problem for NBA. With multiple...