Propositional dynamic logic of looping and converse is elementarily decidable
From MaRDI portal
Publication:3662639
DOI10.1016/S0019-9958(82)91258-XzbMath0515.68062MaRDI QIDQ3662639
Publication date: 1982
Published in: Information and Control (Search for Journal in Brave)
satisfiability problempropositional dynamic logicinfinite treesdeterministic two-way automataelementarily decidable
Related Items
CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus, Verification of \(\mathrm{EB}^3\) specifications using CADP, A branching time logic with past operators, Automata-theoretic techniques for modal logics of programs, Model checking transactional memories, The mu-calculus and Model Checking, Communication in concurrent dynamic logic, Interpreting logics of knowledge in propositional dynamic logic, Compositional verification of concurrent systems by combining bisimulations, Propositional dynamic logic with recursive programs, Uniform inevitability is tree automaton ineffable, Dynamic logic with program specifications and its relational proof system, An automata theoretic decision procedure for the propositional mu- calculus, Branching-time logics with path relativisation, Index appearance record with preorders, Compositional synthesis of control barrier certificates for networks of stochastic systems against \(\omega\)-regular specifications, From bidirectionality to alternation., Cartesian difference categories, Unnamed Item, Mathematical modal logic: A view of its evolution, Program schemata technique for propositional program logics: a 30-year history, Determinism and looping in combinatory PDL, Linear temporal logic symbolic model checking, Computation Tree Regular Logic for Genetic Regulatory Networks, Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra, A unified approach for showing language inclusion and equivalence between various types of \(\omega\)-automata, Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities, Gentzen-type axiomatization for PAL, A modal logic for cyclic repeating, Combining partial-order reductions with on-the-fly model-checking., On the descriptional complexity of finite automata with modified acceptance conditions, Bridging the gap between fair simulation and trace inclusion, Nondeterministic program schemata and their relation to dynamic logic, CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks, Decision procedures and expressiveness in the temporal logic of branching time, Model checking propositional dynamic logic with all extras, Temporal logics with language parameters, From Philosophical to Industrial Logics, Verification of concurrent programs: The automata-theoretic framework, An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps, From Monadic Logic to PSL, A Rice-style theorem for parallel automata, The power of a propositional constant, Unnamed Item, 2-Exp Time lower bounds for propositional dynamic logics with intersection, Decidability and Expressivity of Ockhamist Propositional Dynamic Logics, \( \omega \)-automata, Automata on infinite trees, Streett Automata Model Checking of Higher-Order Recursion Schemes, A Theory of Bounded Fair Scheduling, On qualitative route descriptions. Representation, agent models, and computational complexity, Propositional dynamic logic with local assignments, Rabin vs. Streett Automata, An essay in combinatory dynamic logic, Compositional verification of asynchronous concurrent systems using CADP
