From Philosophical to Industrial Logics

DOI10.1007/978-3-540-92701-3_7MaRDI QIDQ3601803zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• From Löwenheim to PSL and SVA
• From Church and Prior to PSL
• From Monadic Logic to PSL
• The Beginning of Model Checking: A Personal Perspective
• Automata- and logic-based systems design

Cites work

• 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 finite-state concurrent systems using temporal logic specifications
• Automatic Verification of Sequential Circuits Using Temporal Logic
• 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
• Fifteen Years of Formal Property Verification in Intel
• 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
• 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 3715502 (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 50008 (Why is no real title available?)
• scientific article; zbMATH DE number 177248 (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 3591965 (Why is no real title available?)
• scientific article; zbMATH DE number 734956 (Why is no real title available?)
• scientific article; zbMATH DE number 1956573 (Why is no real title available?)
• scientific article; zbMATH DE number 1964695 (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 3254905 (Why is no real title available?)
• scientific article; zbMATH DE number 3271460 (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?)
• Looping vs. repeating in dynamic logic
• Modal 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 classical decision problem.
• 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 alternating automata are not that weak
• Weak Second‐Order Arithmetic and Finite Automata
• “Sometimes” and “not never” revisited

Cited in

(9)

• The compound interest in relaxing punctuality
• Data-driven and model-based verification via Bayesian identification and reachability analysis
• On weighted first-order logics with discounting
• Monitoring metric first-order temporal properties
• From Church and Prior to PSL
• Specification languages for stutter-invariant regular properties
• From Monadic Logic to PSL
• From Löwenheim to PSL and SVA
• Improved decision procedures for multi-modal tense logic using CEGAR-tableaux

Describes a project that uses

Uses Software

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

This page was built for publication: From Philosophical to Industrial Logics

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