Propositional dynamic logic of regular programs
From MaRDI portal
Publication:1258296
DOI10.1016/0022-0000(79)90046-1zbMath0408.03014MaRDI QIDQ1258296
Michael J. Fischer, Richard E. Ladner
Publication date: 1979
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(79)90046-1
Semantics; Turing Machine; Equivalence of Regular Expressions; Propositional Dynamic Logic of Regular Programs; Propositional Modal Logic; Simple One-Tape Turing Machines
03B45: Modal logic (including the logic of norms)
03B60: Other nonclassical logic
68Q65: Abstract data types; algebraic specification
68N01: General topics in the theory of software
03D10: Turing machines and related notions
68W99: Algorithms in computer science
Related Items
Reasoning about common knowledge with infinitely many agents, A description logic based situation calculus, Games for the \(\mu\)-calculus, Logical analysis of demonic nondeterministic programs, The expressive power of implicit specifications, Gentzen-type axiomatization for PAL, Propositional dynamic logic of nonregular programs, A probabilistic dynamic logic, The propositional dynamic logic of deterministic, well-structured programs, Results on the propositional \(\mu\)-calculus, Undecidability of PDL with \(L=\{a^{2^ i}| i\geq 0\}\), Decidability of finite probabilistic propositional dynamic logics, Propositional dynamic logic of context-free programs and fixpoint logic with chop, Branching versus linear logics yet again, A uniform method for proving lower bounds on the computational complexity of logical theories, Determinism and looping in combinatory PDL, Deciding expressive description logics in the framework of resolution, Local variable scoping and Kleene algebra with tests, Cut-free sequent systems for temporal logic, Canonical completeness of infinitary \(\mu \), A note on an extension of PDL, Alternating-time stream logic for multi-agent systems, On the proof theory of the modal mu-calculus, On combinations of propositional dynamic logic and doxastic modal logics, Polyadic dynamic logics for HPSG parsing, A multiprocess network logic with temporal and spatial modalities, Process logic with regular formulas, Propositional dynamic logic with local assignments, A probabilistic PDL, PDL with data constants, The semantics of Hoare's iteration rule, A logic to reason about likelihood, Automata-theoretic techniques for modal logics of programs, Concurrent program schemes and their logics, Communication in concurrent dynamic logic, Interpreting logics of knowledge in propositional dynamic logic, Succinct representation of regular sets using gotos and Boolean variables, Alternating multihead finite automata, A finite model theorem for the propositional \(\mu\)-calculus, An arithmetical hierarchy in propositional dynamic logic, An automata theoretic decision procedure for the propositional mu- calculus, An elementary proof of the completeness of PDL, Propositional dynamic logic is weaker without tests, Process logic: Expressiveness, decidability, completeness, On the computational complexity of satisfiability in propositional logics of programs, TABLEAUX: A general theorem prover for modal logics, On models for propositional dynamic logic, Dynamic algebras: Examples, constructions, applications, A model checker for linear time temporal logic, A guide to completeness and complexity for modal logics of knowledge and belief, Getting started: Beginnings in the logic of action, Dynamic linear time temporal logic, Computation paths logic: An expressive, yet elementary, process logic, \(\Pi_ 1^ 1\)-universality of some propositional logics of concurrent programs, A modal perspective on the computational complexity of attribute value grammar, CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus, Complexity results for two-way and multi-pebble automata and their logics, The complexity of PDL with interleaving, Complexity of equations valid in algebras of relations. I: Strong non-finitizability, Modeling belief in dynamic systems. I: Foundations, Program schemata vs. automata for decidability of program logics, A polynomial space construction of tree-like models for logics with local chains of modal connectives, Complexity of some problems in positive and related calculi, Mathematical modal logic: A view of its evolution, Symbolic model checking for \(\mu\)-calculus requires exponential time, EXPtime tableaux for ALC, On the completeness of propositional Hoare logic, Interactions between knowledge, action and commitment within agent dynamic logic, About cut elimination for logics of common knowledge, A linear-time model-checking algorithm for the alternation-free modal mu- calculus, The price of universality, Domino-tiling games, Deterministic propositional dynamic logic: finite models, complexity, and completeness, Combining deduction and model checking into tableaux and algorithms for converse-PDL., Module checking, Tarskian set constraints, On the structural simplicity of machines and languages, Decision procedures and expressiveness in the temporal logic of branching time, On the universal and existential fragments of the \(\mu\)-calculus, Symbolic model checking for channel-based component connectors, Path constraints in semistructured data, Reasoning on UML class diagrams, A tableau decision procedure for \(\mathcal{SHOIQ}\), A sequent calculus for logic of knowledge and past time: completeness and decidability, The complexity of finite model reasoning in description logics, Model checking propositional dynamic logic with all extras, On complexity of verification of interacting agents' behavior, Characterizing EF and EX tree logics, Complexity of modal logics with Presburger constraints, A propositional logic of Boolean recursive programs in which predicate variables appear in conditions, Mechanizing common knowledge logic using COQ, Propositional dynamic logic with recursive programs, Complexity analysis of propositional concurrent programs using domino tiling, REASONING ABOUT TRANSFINITE SEQUENCES, Computation Tree Regular Logic for Genetic Regulatory Networks, The Complexity of Model Checking for Intuitionistic Logics and Their Modal Companions, An Automata-Theoretic Approach to Infinite-State Systems, From Philosophical to Industrial Logics, Game Quantification Patterns, PDL with intersection and converse: satisfiability and infinite-state model checking, On the Decision Problem for Two-Variable First-Order Logic, A new proof of completeness for a relative modal logic with composition and intersection, Formal verification of multi-agent systems behaviour emerging from cognitive task analysis, Complexity of interpolation and related problems in positive calculi, Unnamed Item, A multi-dimensional terminological knowledge representation language, Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski, An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability, Propositional Dynamic Logic for Message-Passing Systems, From Monadic Logic to PSL, 2-Exp Time lower bounds for propositional dynamic logics with intersection, Terminating Tableaux for Hybrid Logic with Eventualities, Description Logics, Logical Foundations of XML and XQuery, PDL with intersection of programs: a complete axiomatization, A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time, Complexity of intuitionistic propositional logic and its fragments, THE COMPLEXITY OF SATISFIABILITY FOR FRAGMENTS OF CTL AND CTL⋆, A first step towardsmodeling semistructured data in hybrid multimodal logic, PDL for ordered trees, PDL with negation of atomic programs, KAT-ML: an interactive theorem prover for Kleene algebra with tests, Classifying the computational complexity of problems, Semantics of looping programs in Propositional Dynamic Logic, What is an inference rule?, Complete Axiomatization of a Relative Modal Logic with Composition and Intersection
Cites Work
- Theory of program structures: Schemes, semantics, verification
- Consistent and complementary formal theories of the semantics of programming languages
- On static logics, dynamic logics, and complexity classes
- Guarded commands, nondeterminacy and formal derivation of programs
- The Computational Complexity of Provability in Systems of Modal Propositional Logic
- A practical decision method for propositional dynamic logic (Preliminary Report)
- An axiomatic basis for computer programming
- Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
