From Monadic Logic to PSL

DOI10.1007/978-3-540-78127-1_36zbMATH Open1133.68380OpenAlexW1524770419MaRDI QIDQ5452203FDOQ5452203

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) History of computer science (68-03) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

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

Cited In (3)

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

This page was built for publication: From Monadic Logic to PSL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5452203)