Tableau-based automata construction for dynamic linear time temporal logic

DOI10.1007/S10472-006-9020-7zbMATH Open1112.03014OpenAlexW2091562580WikidataQ58207624 ScholiaQ58207624MaRDI QIDQ862830FDOQ862830

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

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

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)

Cites Work

• The complexity of propositional linear temporal logics
• Temporal logic can be more expressive
• Planning for temporally extended goals.
• Title not available (Why is that?)
• Reasoning about infinite computations
• Title not available (Why is that?)
• Title not available (Why is that?)
• Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications
• Reasoning about actions in dynamic linear time temporal logic
• Dynamic linear time temporal logic
• Logics in Artificial Intelligence
• Specifying and verifying systems of communicating agents in a temporal action logic

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
• Title not available (Why is that?)

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)