Monodic temporal logic with quantified propositional variables
This paper considers first-order linear temporal logic (FO-LTL) and studies its extensions with propositional quantification and right-linear grammar operators. The focus is on decidability and recursive enumerability of these extensions. For that purpose, the authors restrict themselves to a decidable fragment of FO-LTL, that is, the monodic fragment of FO-LTL. A formula is monodic if modal formulas contain at most one free individual variable. The authors show that unsatisfiability is recursively enumerable for the monodic fragment where propositional quantification occurs outside of quantification of individual variables (and grammar operators), inside of which externally quantified propositions are within positive occurrences of existential quantifiers for individual variables in the overall formula. As a second result, the authors show that satisfiability is recursively enumerable and decidable when the number of individual variables is restricted to two. Without this condition, it is shown that even with severe restrictions on the first-order part of the logic, no non-trivial prefix class is recursively enumerable.
- Decidable cases of first-order temporal logic with functions
- One-variable first-order linear temporal logics with counting
- PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic
- On Non-local Propositional and Weak Monodic Quantified CTL*
- Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
- Monitor Logics for Quantitative Monitor Automata
- Monodic fragments of probabilistic first-order logic
- On the decidability of a fragment of preferential LTL
- A decidable and expressive fragment of many-sorted first-order linear temporal logic
This page was built for publication: Monodic temporal logic with quantified propositional variables
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2893321)
