A decidable timeout-based extension of linear temporal logic

DOI10.1080/11663081.2014.964491MaRDI QIDQ4583356zbMATH OpenOpenAlexFDO

Authors Janardan Misra, Suman Roy

Publication date 28 August 2018

Published in Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1080/11663081.2014.964491

zbMATH Keywords

expressiveness of logicsmodel checkingreal-time logicstableau satisfiabilitytemporal logicstimeout constraintstimeout modelstiming propertiesundecidability

Mathematics Subject Classification ID

Temporal logic (03B44) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Logic in computer science (03B70) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A really temporal logic
• Model-checking timed temporal logics
• scientific article; zbMATH DE number 1927567
• Model-checking in dense real-time
• Translating a continuous-time temporal logic into timed automata.

Cites work

• A really temporal logic
• A theory of timed automata
• Computer Aided Verification
• Formal description techniques and protocol specification, testing and verification. FORTE XI/ PSTV XVIII '98. IFIP TC6 WG6. 1 joint international conference on Formal description techniques for distributed systems and communication protocols (FORTE XI) an
• Formal Methods for the Design of Real-Time Systems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• scientific article; zbMATH DE number 4128370 (Why is no real title available?)
• scientific article; zbMATH DE number 1339873 (Why is no real title available?)
• scientific article; zbMATH DE number 1500644 (Why is no real title available?)
• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• scientific article; zbMATH DE number 3237829 (Why is no real title available?)
• Real-time logics: Complexity and expressiveness
• Real-Time Systems
• Relationships between nondeterministic and deterministic tape complexities
• Some Recent Results in Metric Temporal Logic
• The complexity of propositional linear temporal logics
• Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems
• What good are digital clocks?

Cited in

(5)

• Three Approaches to Timed External Choice in UTP
• scientific article; zbMATH DE number 1956573 (Why is no real title available?)
• scientific article; zbMATH DE number 2064461 (Why is no real title available?)
• scientific article; zbMATH DE number 1927567 (Why is no real title available?)
• scientific article; zbMATH DE number 2090022 (Why is no real title available?)

Describes a project that uses

Uses Software

• Uppaal
• SPIN

This page was built for publication: A decidable timeout-based extension of linear temporal logic

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