Propositional dynamic logic of regular programs

From MaRDI portal

Publication:1258296

Jump to:navigation, search

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

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

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

Unnamed Item, A multi-dimensional terminological knowledge representation language, Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski, Propositional Dynamic Logic for Message-Passing Systems, From Monadic Logic to PSL, 2-Exp Time lower bounds for propositional dynamic logics with intersection, 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, Reasoning about common knowledge with infinitely many agents, 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, 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, On the proof theory of the modal mu-calculus, On combinations of propositional dynamic logic and doxastic modal logics, 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, 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, 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, From Philosophical to Industrial Logics, Game Quantification Patterns, PDL with intersection and converse: satisfiability and infinite-state model checking, 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

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