Specification and verification using temporal logics

DOI10.1142/9789814271059_0015MaRDI QIDQ4907867zbMATH OpenOpenAlexFDO

Authors Stéphane Demri, Paul Gastin

Publication date 26 February 2013

Published in Modern Applications of Automata Theory (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1142/9789814271059_0015

zbMATH Keywords

automatalineartime temporal logicspecificationtemporal operatorsverification

Mathematics Subject Classification ID

Temporal logic (03B44) Automata and formal grammars in connection with logical questions (03D05) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Temporal logic and state systems
• An introduction to practical formal methods using temporal logic
• Automata- and logic-based systems design
• From LTL to Symbolically Represented Deterministic Automata
• Temporal logics in computer science. Finite-state systems

Cited in

(20)

• Loop-check specification for a sequent calculus of temporal logic
• Event-driven temporal logic pattern for control software requirements specification
• Verification
• Parameterized model checking of weighted networks
• Using temporal logics of knowledge for specification and verification -- a case study
• Using Locales to Define a Rely-Guarantee Temporal Logic
• scientific article; zbMATH DE number 6117314 (Why is no real title available?)
• Temporal Logic Verification of Lock-Freedom
• Complementary Criteria for Testing Temporal Logic Properties
• scientific article; zbMATH DE number 4081518 (Why is no real title available?)
• scientific article; zbMATH DE number 4089533 (Why is no real title available?)
• scientific article; zbMATH DE number 148938 (Why is no real title available?)
• scientific article; zbMATH DE number 1231598 (Why is no real title available?)
• TEMPORAL LOGICS FOR TRACE SYSTEMS: ON AUTOMATED VERIFICATION
• scientific article; zbMATH DE number 4119598 (Why is no real title available?)
• A language-theoretic view of verification
• LTL-specification of bounded counter machines
• Revising system specifications in temporal logic
• Are bundles good deals for first-order modal logic?
• First order Büchi automata and their application to verification of LTL specifications

This page was built for publication: Specification and verification using temporal logics

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