Tableau-based automata construction for dynamic linear time temporal logic

DOI10.1007/s10472-006-9020-7zbMath1112.03014OpenAlexW2091562580WikidataQ58207624 ScholiaQ58207624MaRDI QIDQ862830

Alberto Martelli, Laura Giordano

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 logicBüchi automatontableau-based algorithm

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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Reasoning about actions with Temporal Answer Sets ⋮ Formal Verification for Components and Connectors ⋮ Verifying Agents’ Conformance with Multiparty Protocols

Uses Software

• SPIN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Dynamic linear time temporal logic
• Reasoning about infinite computations
• Planning for temporally extended goals.
• Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications
• Reasoning about actions in dynamic linear time temporal logic
• Temporal logic can be more expressive
• The complexity of propositional linear temporal logics
• Logics in Artificial Intelligence
• AI*IA 2003: Advances in Artificial Intelligence

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