Tableau-based automata construction for dynamic linear time temporal logic

DOI10.1007/S10472-006-9020-7MaRDI QIDQ862830zbMATH OpenOpenAlexWikidataFDO

Authors Laura Giordano, Alberto Martelli

Publication date 24 January 2007

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10472-006-9020-7

zbMATH Keywords

model checkingtemporal logictableau-based algorithmBüchi automaton

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 6401143
• Dynamic linear time temporal logic
• scientific article; zbMATH DE number 1696514
• An improved on-the-fly tableau construction for a real-time temporal logic.
• LTL semantic tableaux and alternating \(\omega\)-automata via linear factors

Cites work

• scientific article; zbMATH DE number 89002 (Why is no real title available?)
• scientific article; zbMATH DE number 2064229 (Why is no real title available?)
• scientific article; zbMATH DE number 2102710 (Why is no real title available?)
• Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications
• Dynamic linear time temporal logic
• Logics in Artificial Intelligence
• Planning for temporally extended goals.
• Reasoning about actions in dynamic linear time temporal logic
• Reasoning about infinite computations
• Specifying and verifying systems of communicating agents in a temporal action logic
• Temporal logic can be more expressive
• The complexity of propositional linear temporal logics

Cited in

(5)

• Formal Verification for Components and Connectors
• A tableau construction for finite linear-time temporal logic
• Reasoning about actions with Temporal Answer Sets
• Verifying Agents’ Conformance with Multiparty Protocols
• scientific article; zbMATH DE number 1696514 (Why is no real title available?)

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: Tableau-based automata construction for dynamic linear time temporal logic

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