Automata-theoretic techniques for modal logics of programs

DOI10.1016/0022-0000(86)90026-7zbMath0622.03017OpenAlexW2033071128MaRDI QIDQ1090675

Publication date: 1986

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0022-0000(86)90026-7

zbMATH Keywords

dynamic logic Büchi automata converse construct deterministic PDL of flowcharts emptiness problem for special automata exponential decision procedure loop construct satisfiability problem for logics subtree automata

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Abstract data types; algebraic specification (68Q65) Decidability of theories and sets of sentences (03B25)

Related Items (88)

On Composing Finite Forests with Modal Logics ⋮ Automated Verification of Parallel Nested DFS ⋮ Type reconstruction with recursive types and atomic subtyping ⋮ The complementation problem for Büchi automata with applications to temporal logic ⋮ Employing symmetry reductions in model checking ⋮ Model checking LTL with regular valuations for pushdown systems ⋮ The computational complexity of scenario-based agent verification and design ⋮ Parameterized model checking of rendezvous systems ⋮ Automata Theory and Model Checking ⋮ Fast and simple nested fixpoints ⋮ Multi-Valued Reasoning about Reactive Systems ⋮ Somewhat finite approaches to infinite sentences. ⋮ A propositional logic of Boolean recursive programs in which predicate variables appear in conditions ⋮ Propositional dynamic logic with quantification over regular computation sequences ⋮ Propositional dynamic logic with recursive programs ⋮ Ordered multi-stack visibly pushdown automata ⋮ Verifying a signature architecture: a comparative case study ⋮ On the relation between reactive synthesis and supervisory control of non-terminating processes ⋮ Reasoning in fuzzy description logics using automata ⋮ Fixed point characterization of infinite behavior of finite-state systems ⋮ Generalized satisfiability for the description logic $\mathcal{ALC}$ ⋮ One-Pass Tableaux for Computation Tree Logic ⋮ On monitoring linear temporal properties ⋮ Taming strategy logic: non-recurrent fragments ⋮ A polynomial space construction of tree-like models for logics with local chains of modal connectives ⋮ Reasoning about Quality and Fuzziness of Strategic Behaviors ⋮ An algorithmic approach for checking closure properties of Ω-regular languages ⋮ Early detection of temporal constraint violations ⋮ Distributed breadth-first search LTL model checking ⋮ On the Decision Problem for Two-Variable First-Order Logic ⋮ Complexity of synthesis of composite service with correctness guarantee ⋮ \textit{Once} and \textit{for all} ⋮ A finite state intersection approach to propositional satisfiability ⋮ Program schemata technique for propositional program logics: a 30-year history ⋮ Inference of $\omega$-languages from prefixes. ⋮ The complexity of computing the behaviour of lattice automata on infinite trees ⋮ Automata-Based Axiom Pinpointing ⋮ Program equivalence checking by two-tape automata ⋮ Decidability of a partial order based temporal logic ⋮ Deciding properties of integral relational automata ⋮ Finite-word hyperlanguages ⋮ On automata on infinite trees ⋮ Interval logics and their decision procedures. I: An interval logic ⋮ Verification of well-formed communicating recursive state machines ⋮ On the equivalence of recursive and nonrecursive Datalog programs ⋮ Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics ⋮ Generalized Satisfiability for the Description Logic $\mathcal{ALC}$ ⋮ Automata can show PSpace results for description logics ⋮ Verification of scope-dependent hierarchical state machines ⋮ A model checker for linear time temporal logic ⋮ Tableaux and algorithms for Propositional Dynamic Logic with Converse ⋮ Reasoning and Query Answering in Description Logics ⋮ A resolution calculus for the branching-time temporal logic CTL ⋮ Answering regular path queries in expressive description logics via alternating tree-automata ⋮ An approach to infinitary temporal proof theory ⋮ Pushdown module checking ⋮ The Quest for a Tight Translation of Büchi to co-Büchi Automata ⋮ Logics for Two Fragments beyond the Syllogistic Boundary ⋮ An Automata-Theoretic Approach to Infinite-State Systems ⋮ Reasoning about XML with temporal logics and automata ⋮ Automata-based axiom pinpointing ⋮ Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse ⋮ Model checking propositional dynamic logic with all extras ⋮ A continuous–discontinuous second‐order transition in the satisfiability of random Horn‐SAT formulas ⋮ A Refined Resolution Calculus for CTL ⋮ An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability ⋮ Tree regular model checking: a simulation-based approach ⋮ Finite-word hyperlanguages ⋮ Variable and Clause Ordering in an FSA Approach to Propositional Satisfiability ⋮ Automata on infinite trees with counting constraints ⋮ Survey on Directed Model Checking ⋮ PDL with intersection and converse: satisfiability and infinite-state model checking ⋮ Matching Trace Patterns with Regular Policies ⋮ Power of Randomization in Automata on Infinite Strings ⋮ Advanced Ramsey-Based Büchi Automata Inclusion Testing ⋮ Ontologies and Databases: The DL-Lite Approach ⋮ An algorithmic approach for checking closure properties of temporal logic specifications and $\omega$-regular languages ⋮ PDL for ordered trees ⋮ PDL with negation of atomic programs ⋮ Alternating automata: Unifying truth and validity checking for temporal logics ⋮ EXPtime tableaux for ALC ⋮ Relating word and tree automata ⋮ Combining deduction and model checking into tableaux and algorithms for converse-PDL. ⋮ Module checking ⋮ Good-for-Game QPTL: An Alternating Hodges Semantics ⋮ Combining interval-based temporal reasoning with general TBoxes ⋮ Model checking dynamic pushdown networks ⋮ Back to the future: a fresh look at linear temporal logic

Cites Work

This page was built for publication: Automata-theoretic techniques for modal logics of programs