From Monadic Logic to PSL

DOI10.1007/978-3-540-78127-1_36zbMath1133.68380OpenAlexW1524770419MaRDI QIDQ5452203

Moshe Y. Vardi

Publication date: 25 March 2008

Published in: Pillars of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-78127-1_36

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) History of computer science (68-03)

Related Items

Linear temporal logic symbolic model checking ⋮ Regular Expressions with Counting: Weak versus Strong Determinism ⋮ Deterministic regular expressions with back-references

Cites Work

• Quantifier elimination in a problem of logical design
• The propositional dynamic logic of deterministic, well-structured programs
• Results on the propositional \(\mu\)-calculus
• Process logic with regular formulas
• Hierarchical verification of asynchronous circuits using temporal logic
• The complementation problem for Büchi automata with applications to temporal logic
• A near-optimal method for reasoning about action
• Process logic: Expressiveness, decidability, completeness
• Symbolic model checking: \(10^{20}\) states and beyond
• Finiteness is mu-ineffable
• Propositional dynamic logic of regular programs
• Reasoning about infinite computations
• Temporal logic. From ancient ideas to artificial intelligence
• More on looping vs. repeating in dynamic logic
• Decision procedures and expressiveness in the temporal logic of branching time
• First-order logic with two variables and unary temporal logic
• Modality and quantification in S5
• A completeness theorem in modal logic
• Weak Second‐Order Arithmetic and Finite Automata
• Temporal logic can be more expressive
• Looping vs. repeating in dynamic logic
• Verification Technology Transfer
• Weak alternating automata are not that weak
• The Büchi Complementation Saga
• Propositional dynamic logic of looping and converse is elementarily decidable
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• Automatic Verification of Sequential Circuits Using Temporal Logic
• “Sometimes” and “not never” revisited
• The complexity of propositional linear temporal logics
• Decision Problems of Finite Automata Design and Related Arithmetics
• Formal verification of parallel programs
• Star-free regular sets of ω-sequences
• On the synthesis of strategies in infinite games
• A topological characterization of weakness
• Nondeterminism and the size of two way finite automata
• A practical decision method for propositional dynamic logic (Preliminary Report)
• Automata-Theoretic Model Checking Revisited
• Correct Hardware Design and Verification Methods
• Solving Sequential Conditions by Finite-State Strategies
• Algorithmic properties of structures
• Safraless Compositional Synthesis
• Computer Aided Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item