Propositional dynamic logic of regular programs

DOI10.1016/0022-0000(79)90046-1zbMath0408.03014OpenAlexW2069709605MaRDI 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

zbMATH Keywords

Semantics Turing Machine Equivalence of Regular Expressions Propositional Dynamic Logic of Regular Programs Propositional Modal Logic Simple One-Tape Turing Machines

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Other nonclassical logic (03B60) Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01) Turing machines and related notions (03D10) Algorithms in computer science (68W99)

Related Items (only showing first 100 items - show all)

The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes ⋮ Parametrised Complexity of Satisfiability in Temporal Logic ⋮ Nested Regular Expressions Can Be Compiled to Small Deterministic Nested Word Automata ⋮ Complexity of interpolation and related problems in positive calculi ⋮ Unnamed Item ⋮ On proving properties of completion strategies ⋮ Undecidability of QLTL and QCTL with two variables and one monadic predicate letter ⋮ A separation theorem for discrete-time interval temporal logic ⋮ Branching-time logics and fairness, revisited ⋮ Deciding the unguarded modal -calculus ⋮ A Decidable Multi-agent Logic for Reasoning About Actions, Instruments, and Norms ⋮ To be announced ⋮ A product version of dynamic linear time temporal logic ⋮ A logical analysis of instrumentality judgments: means-end relations in the context of experience and expectations ⋮ What is an inference rule? ⋮ Satisfiability of quantitative probabilistic CTL: rise to the challenge ⋮ Deontic paradoxes in Mīmāṃsā logics: there and back again ⋮ Dynamic modal logic with counting: when reduction axioms work and fail ⋮ Temporal stream logic modulo theories ⋮ Dynamic epistemic logics for abstract argumentation ⋮ Deciding Equations in the Time Warp Algebra ⋮ A dynamic logic with branching modalities ⋮ Logic of visibility in social networks ⋮ Local completeness logic on Kleene algebra with tests ⋮ On the complexity of Kleene algebra with domain ⋮ Classifying the computational complexity of problems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A multi-dimensional terminological knowledge representation language ⋮ On the Decision Problem for Two-Variable First-Order Logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Propositional Dynamic Logic for Message-Passing Systems ⋮ Unnamed Item ⋮ Towards Metric Temporal Answer Set Programming ⋮ Complexity results for multi-pebble automata and their logics ⋮ Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic ⋮ Tableaux and algorithms for Propositional Dynamic Logic with Converse ⋮ Temporal Logic with Recursion. ⋮ Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities ⋮ An operational domain-theoretic treatment of recursive types ⋮ Propositional Dynamic Logic with Storing, Recovering and Parallel Composition ⋮ Terminating Tableaux for Hybrid Logic with Eventualities ⋮ The satisfiability problem for a quantitative fragment of PCTL ⋮ An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability ⋮ Temporal logics with language parameters ⋮ Dynamic logic as a uniform framework for theorem proving in intensional logic ⋮ A linear-time model-checking algorithm for the alternation-free modal mu-calculus ⋮ Unnamed Item ⋮ Axiomatization and computability of a variant of iteration-free PDL with fork ⋮ Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski ⋮ From Monadic Logic to PSL ⋮ A new proof of completeness for a relative modal logic with composition and intersection ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ Propositional Dynamic Logic for Hyperproperties ⋮ 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⋆ ⋮ An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability ⋮ 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 ⋮ Formal verification of multi-agent systems behaviour emerging from cognitive task analysis ⋮ 2-Exp Time lower bounds for propositional dynamic logics with intersection ⋮ Computation paths logic: An expressive, yet elementary, process logic ⋮ Alternating automata: Unifying truth and validity checking for temporal logics ⋮ Complete Axiomatization of a Relative Modal Logic with Composition and Intersection ⋮ On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic ⋮ Semantics of looping programs in Propositional Dynamic Logic ⋮ Bisimilar and logically equivalent programs in PDL with parallel operator ⋮ On the universal and existential fragments of the \(\mu\)-calculus ⋮ Some modal aspects of XPath ⋮ The satisfiability problem for a quantitative fragment of PCTL ⋮ Sequent calculi for branching time temporal logics of knowledge and beliefwith awareness: completeness and decidability ⋮ Functional Specification of Hardware via Temporal Logic ⋮ The mu-calculus and Model Checking ⋮ Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition ⋮ Unnamed Item ⋮ Adding proof calculi to epistemic logics with structured knowledge ⋮ A Poor Man’s Epistemic Logic Based on Propositional Assignment and Higher-Order Observation ⋮ Trace Semantics for IPDL ⋮ Tableaux for Single-Agent Epistemic PDL with Perfect Recall and No Miracles ⋮ Algebraic Semantics for Dynamic Dynamic Logic ⋮ Compositional verification of concurrent systems by combining bisimulations ⋮ Complexity of modal logics with Presburger constraints ⋮ Complexity of finite-variable fragments of propositional temporal and modal logics of computation ⋮ A propositional logic of Boolean recursive programs in which predicate variables appear in conditions ⋮ A Propositional Dynamic Logic for Concurrent Programs Based on the π-Calculus ⋮ Propositional dynamic logic with quantification over regular computation sequences ⋮ Mechanizing common knowledge logic using COQ ⋮ Propositional dynamic logic with recursive programs ⋮ Symbolic model checking for channel-based component connectors ⋮ A modal view on resource-bounded propositional logics ⋮ A family of dynamic description logics for representing and reasoning about actions ⋮ A formalism to specify unambiguous instructions inspired by Mīmāṁsā in computational settings

Cites Work

This page was built for publication: Propositional dynamic logic of regular programs