Propositional dynamic logic of regular programs

From MaRDI portal

Publication:1258296

Jump to:navigation, search

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

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 ⋮ 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 ⋮ CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus ⋮ The semantics of Hoare's iteration rule ⋮ Bisimilar and logically equivalent programs in PDL ⋮ Extending propositional dynamic logic for Petri nets ⋮ Bounded situation calculus action theories ⋮ Completeness and decidability results for CTL in constructive type theory ⋮ A logic to reason about likelihood ⋮ Automata-theoretic techniques for modal logics of programs ⋮ Concurrent program schemes and their logics ⋮ The undecidability of quantified announcements ⋮ Communication in concurrent dynamic logic ⋮ Interpreting logics of knowledge in propositional dynamic logic ⋮ Propositional dynamic logic of context-free programs and fixpoint logic with chop ⋮ Complexity results for two-way and multi-pebble automata and their logics ⋮ The complexity of PDL with interleaving ⋮ The \(\mu\)-calculus alternation depth hierarchy is infinite over finite planar graphs ⋮ Succinct representation of regular sets using gotos and Boolean variables ⋮ ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching ⋮ 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 ⋮ Reasoning about common knowledge with infinitely many agents ⋮ Finite-trace linear temporal logic: coinductive completeness ⋮ Complexity of equations valid in algebras of relations. I: Strong non-finitizability ⋮ Action emulation ⋮ A description logic based situation calculus ⋮ Branching-time logics with path relativisation ⋮ Modeling belief in dynamic systems. I: Foundations ⋮ Program schemata vs. automata for decidability of program logics ⋮ On the complexity of input/output logic ⋮ 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 ⋮ An elementary proof of the completeness of PDL ⋮ Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs ⋮ Propositional dynamic logic is weaker without tests ⋮ Complexity of synthesis of composite service with correctness guarantee ⋮ \textit{Once} and \textit{for all} ⋮ Branching versus linear logics yet again ⋮ A uniform method for proving lower bounds on the computational complexity of logical theories ⋮ Mathematical modal logic: A view of its evolution ⋮ Determinism and looping in combinatory PDL ⋮ Process logic: Expressiveness, decidability, completeness ⋮ Reasoning about permitted announcements ⋮ On the computational complexity of satisfiability in propositional logics of programs ⋮ Deciding expressive description logics in the framework of resolution ⋮ Linear temporal logic symbolic model checking ⋮ Reasoning about plan revision in BDI agent programs ⋮ Propositional dynamic logic for searching games with errors ⋮ Temporal logics for concurrent recursive programs: satisfiability and model checking ⋮ Local variable scoping and Kleene algebra with tests ⋮ Public announcement logic with distributed knowledge: expressivity, completeness and complexity ⋮ TABLEAUX: A general theorem prover for modal logics ⋮ On models for propositional dynamic logic ⋮ The complexity of debate checking ⋮ Cut-free sequent systems for temporal logic ⋮ Canonical completeness of infinitary \(\mu \) ⋮ Games for the \(\mu\)-calculus ⋮ Logical analysis of demonic nondeterministic programs ⋮ Dynamic algebras: Examples, constructions, applications ⋮ Epistemic protocols for dynamic gossip ⋮ A model checker for linear time temporal logic ⋮ A guide to completeness and complexity for modal logics of knowledge and belief ⋮ Completely and partially executable sequences of actions in deontic context ⋮ Visibly linear temporal logic ⋮ Complexity of validity for propositional dependence logics ⋮ Parametric linear dynamic logic ⋮ An algebraic approach to multirelations and their properties ⋮ Rewrite rules for \(\mathrm{CTL}^\ast\) ⋮ The expressive power of implicit specifications ⋮ A note on an extension of PDL ⋮ Gentzen-type axiomatization for PAL ⋮ A calculus for automatic verification of Petri nets based on resolution and dynamic logics ⋮ Getting started: Beginnings in the logic of action ⋮ Alternating-time stream logic for multi-agent systems ⋮ CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks ⋮ Interactions between knowledge, action and commitment within agent dynamic logic ⋮ About cut elimination for logics of common knowledge ⋮ 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 ⋮ Symbolic model checking for \(\mu\)-calculus requires exponential time ⋮ Dynamic linear time temporal logic ⋮ Computation paths logic: An expressive, yet elementary, process logic ⋮ Propositional dynamic logic of nonregular programs ⋮ A probabilistic dynamic logic ⋮ EXPtime tableaux for ALC ⋮ A multiprocess network logic with temporal and spatial modalities ⋮ Process logic with regular formulas ⋮ 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\}\) ⋮ \(\Pi_ 1^ 1\)-universality of some propositional logics of concurrent programs ⋮ Propositional dynamic logic with local assignments ⋮ A probabilistic PDL ⋮ A modal perspective on the computational complexity of attribute value grammar ⋮ PDL with data constants ⋮ On the completeness of propositional Hoare logic ⋮ Decidability of finite probabilistic propositional dynamic logics ⋮ Existential second-order logic and modal logic with quantified accessibility relations ⋮ 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 ⋮ On the structural simplicity of machines and languages ⋮ Querying the Unary Negation Fragment with Regular Path Expressions. ⋮ Communicating Finite-State Machines and Two-Variable Logic ⋮ Exponential-Size Model Property for PDL with Separating Parallel Composition ⋮ Efficiently Deciding μ-Calculus with Converse over Finite Trees ⋮ Action models in inquisitive logic ⋮ Cartesian difference categories ⋮ Dynamic Łukasiewicz logic and dynamic MV-algebras ⋮ Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic ⋮ Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism ⋮ Free Kleene algebras with domain ⋮ Program schemata technique for propositional program logics: a 30-year history ⋮ Computation Tree Regular Logic for Genetic Regulatory Networks ⋮ Path constraints in semistructured data ⋮ Reasoning on UML class diagrams ⋮ Temporal logics with language parameters ⋮ A tableau decision procedure for \(\mathcal{SHOIQ}\) ⋮ Quantified Coalition Logic of Knowledge, Belief and Certainty ⋮ Strategies, model checking and branching-time properties in Maude ⋮ The Modal μ-Calculus Caught Off Guard ⋮ Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics ⋮ The complexity of identifying characteristic formulae ⋮ A sequent calculus for logic of knowledge and past time: completeness and decidability ⋮ Answering regular path queries in expressive description logics via alternating tree-automata ⋮ The complexity of finite model reasoning in description logics ⋮ Almost event-rate independent monitoring ⋮ The Complexity of Model Checking for Intuitionistic Logics and Their Modal Companions ⋮ An Automata-Theoretic Approach to Infinite-State Systems ⋮ Decision procedures and expressiveness in the temporal logic of branching time ⋮ Model checking propositional dynamic logic with all extras ⋮ On complexity of verification of interacting agents' behavior ⋮ Producing explanations for rich logics ⋮ The compound interest in relaxing punctuality ⋮ From Philosophical to Industrial Logics ⋮ Game Quantification Patterns ⋮ Characterizing EF and EX tree logics ⋮ Towards reasoning about Petri nets: a propositional dynamic logic based approach ⋮ Computational complexity for bounded distributive lattices with negation ⋮ Dynamic preference logic meets iterated belief change: representation results and postulates characterization ⋮ Inquisitive propositional dynamic logic ⋮ PDL with intersection and converse: satisfiability and infinite-state model checking ⋮ A linear-time model-checking algorithm for the alternation-free modal mu- calculus ⋮ Event-based time-stamped claim logic ⋮ Two AGM-style characterizations of model repair ⋮ Temporal logic with recursion ⋮ ExpTime tableaux with global caching for hybrid PDL ⋮ Satisfiability of Linear Time Mu-Calculus on Finite Traces ⋮ Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition ⋮ Deontology of compound actions ⋮ Complexity of the universal theory of modal algebras ⋮ The price of universality ⋮ Description Logics ⋮ Logical Foundations of XML and XQuery ⋮ Clausal Tableaux for Hybrid PDL ⋮ PDL with intersection of programs: a complete axiomatization ⋮ Domino-tiling games ⋮ Constructive Formalization of Hybrid Logic with Eventualities ⋮ The model checking fingerprints of CTL operators ⋮ Decidability and Expressivity of Ockhamist Propositional Dynamic Logics ⋮ MODAL RESTRICTION SEMIGROUPS: TOWARDS AN ALGEBRA OF FUNCTIONS ⋮ Deterministic propositional dynamic logic: finite models, complexity, and completeness ⋮ Alternating-time temporal logic ATL with finitely bounded semantics ⋮ REASONING ABOUT TRANSFINITE SEQUENCES ⋮ NP reasoning in the monotone \(\mu\)-calculus ⋮ On qualitative route descriptions. Representation, agent models, and computational complexity ⋮ Monadic <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" altimg="si1.gif" overflow="scroll"><mml:msubsup><mml:mi mathvariant="normal">Σ</mml:mi><mml:mn>1</mml:mn><mml:mn>1</mml:mn></mml:msubsup></mml:math> and Modal Logic with Quantified Binary Relations ⋮ Combining deduction and model checking into tableaux and algorithms for converse-PDL. ⋮ Module checking ⋮ Tarskian set constraints ⋮ A semantics and a logic for \textit{Fuzzy Arden Syntax} ⋮ Dynamic Łukasiewicz logic and its application to immune system ⋮ Complexity analysis of propositional concurrent programs using domino tiling ⋮ Compositional verification of asynchronous concurrent systems using CADP ⋮ A goal-directed decision procedure for hybrid PDL

Cites Work

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:1258296&oldid=13353961"