From Philosophical to Industrial Logics

DOI10.1007/978-3-540-92701-3_7zbMath1209.68325OpenAlexW1482831113MaRDI QIDQ3601803

Moshe Y. Vardi

Publication date: 12 February 2009

Published in: Logic and Its Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-92701-3_7

Mathematics Subject Classification ID

Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

Data-driven and model-based verification via Bayesian identification and reachability analysis, On weighted first-order logics with discounting, The compound interest in relaxing punctuality, Monitoring Metric First-Order Temporal Properties, Specification Languages for Stutter-Invariant Regular Properties

Uses Software

• SPIN
• NuSMV
• CESAR
• SPOT
• LTL2BA
• VIS

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
• Fifteen Years of Formal Property Verification in Intel
• 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
• The classical decision problem.
• 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