From Monadic Logic to PSL

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

Authors 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)

Recommendations

• From Church and Prior to PSL
• From Löwenheim to PSL and SVA
• From Philosophical to Industrial Logics
• Theorem Proving in Higher Order Logics
• On regular temporal logics with past

Cites work

• scientific article; zbMATH DE number 1705164 (Why is no real title available?)
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 3427224 (Why is no real title available?)
• scientific article; zbMATH DE number 3129315 (Why is no real title available?)
• scientific article; zbMATH DE number 3137366 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3876574 (Why is no real title available?)
• scientific article; zbMATH DE number 5604077 (Why is no real title available?)
• scientific article; zbMATH DE number 3919813 (Why is no real title available?)
• scientific article; zbMATH DE number 3922633 (Why is no real title available?)
• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 4027441 (Why is no real title available?)
• scientific article; zbMATH DE number 4033710 (Why is no real title available?)
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 3714896 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 177519 (Why is no real title available?)
• scientific article; zbMATH DE number 3469999 (Why is no real title available?)
• scientific article; zbMATH DE number 3492660 (Why is no real title available?)
• scientific article; zbMATH DE number 3510287 (Why is no real title available?)
• scientific article; zbMATH DE number 3591965 (Why is no real title available?)
• scientific article; zbMATH DE number 1956573 (Why is no real title available?)
• scientific article; zbMATH DE number 2038760 (Why is no real title available?)
• scientific article; zbMATH DE number 2080056 (Why is no real title available?)
• scientific article; zbMATH DE number 1479635 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• scientific article; zbMATH DE number 1796144 (Why is no real title available?)
• scientific article; zbMATH DE number 1796153 (Why is no real title available?)
• scientific article; zbMATH DE number 3799616 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 7354705 (Why is no real title available?)
• scientific article; zbMATH DE number 3237829 (Why is no real title available?)
• scientific article; zbMATH DE number 3271460 (Why is no real title available?)
• scientific article; zbMATH DE number 3273196 (Why is no real title available?)
• scientific article; zbMATH DE number 3328724 (Why is no real title available?)
• scientific article; zbMATH DE number 3363520 (Why is no real title available?)
• scientific article; zbMATH DE number 3368555 (Why is no real title available?)
• scientific article; zbMATH DE number 3186871 (Why is no real title available?)
• scientific article; zbMATH DE number 3189696 (Why is no real title available?)
• A completeness theorem in modal logic
• A near-optimal method for reasoning about action
• A practical decision method for propositional dynamic logic (preliminary report)
• A topological characterization of weakness
• Algorithmic properties of structures
• Automata-Theoretic Model Checking Revisited
• Automatic Verification of Sequential Circuits Using Temporal Logic
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Correct Hardware Design and Verification Methods
• Decision Problems of Finite Automata Design and Related Arithmetics
• Decision procedures and expressiveness in the temporal logic of branching time
• Finiteness is mu-ineffable
• First-order logic with two variables and unary temporal logic
• Formal verification of parallel programs
• Graph-Based Algorithms for Boolean Function Manipulation
• Hierarchical verification of asynchronous circuits using temporal logic
• Looping vs. repeating in dynamic logic
• Modality and quantification in S5
• More on looping vs. repeating in dynamic logic
• Nondeterminism and the size of two way finite automata
• On the synthesis of strategies in infinite games
• Process logic with regular formulas
• Process logic: Expressiveness, decidability, completeness
• Propositional dynamic logic of looping and converse is elementarily decidable
• Propositional dynamic logic of regular programs
• Quantifier elimination in a problem of logical design
• Reasoning about infinite computations
• Reasoning with temporal logic on truncated paths.
• Results on the propositional \(\mu\)-calculus
• Safraless Compositional Synthesis
• Solving Sequential Conditions by Finite-State Strategies
• Star-free regular sets of ω-sequences
• Symbolic model checking: \(10^{20}\) states and beyond
• Temporal logic can be more expressive
• Temporal logic. From ancient ideas to artificial intelligence
• The Büchi Complementation Saga
• The complementation problem for Büchi automata with applications to temporal logic
• The complexity of propositional linear temporal logics
• The propositional dynamic logic of deterministic, well-structured programs
• Verification Technology Transfer
• Weak Second‐Order Arithmetic and Finite Automata
• Weak alternating automata are not that weak
• “Sometimes” and “not never” revisited

Cited in

(7)

• Linear temporal logic symbolic model checking
• From Church and Prior to PSL
• From Löwenheim to PSL and SVA
• Regular Expressions with Counting: Weak versus Strong Determinism
• Deterministic regular expressions with back-references
• From Philosophical to Industrial Logics
• Validating the PSL/Sugar semantics using automated reasoning

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)