A Decidable Non-Regular Modal Fixpoint Logic
| Autor: | Bruse, Florian, Lange, Martin |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
formal specification
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES temporal logic TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Computer Science::Programming Languages Theory of computation → Program specifications Theory of computation → Modal and temporal logics expressive power |
| DOI: | 10.4230/lipics.concur.2021.23 |
| Popis: | Fixpoint Logic with Chop (FLC) extends the modal μ-calculus with an operator for sequential composition between predicate transformers. This makes it an expressive modal fixpoint logic which is capable of formalising many non-regular program properties. Its satisfiability problem is highly undecidable. Here we define Visibly Pushdown Fixpoint Logic with Chop, a fragment in which fixpoint formulas are required to be of a certain form resembling visibly pushdown grammars. We give a sound and complete game-theoretic characterisation of FLC’s satisfiability problem and show that the games corresponding to formulas from this fragment are stair-parity games and therefore effectively solvable, resulting in 2EXPTIME-completeness of this fragment. The lower bound is inherited from PDL over Recursive Programs, which is structurally similar but considerably weaker in expressive power. LIPIcs, Vol. 203, 32nd International Conference on Concurrency Theory (CONCUR 2021), pages 23:1-23:18 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|