A decidable timeout-based extension of linear temporal logic

DOI10.1080/11663081.2014.964491zbMATH Open1398.03081OpenAlexW1627271069MaRDI QIDQ4583356FDOQ4583356

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

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.

zbMATH Keywords

model checkingundecidabilitytemporal logicsreal-time logicsexpressiveness of logicstableau satisfiabilitytimeout constraintstimeout modelstiming properties

Mathematics Subject Classification ID

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

Cites Work

• Formal Methods for the Design of Real-Time Systems
• Computer Aided Verification
• A theory of timed automata
• Relationships between nondeterministic and deterministic tape complexities
• Some Recent Results in Metric Temporal Logic
• The complexity of propositional linear temporal logics
• A really temporal logic
• Title not available (Why is that?)
• What good are digital clocks?
• Title not available (Why is that?)
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Real-time logics: Complexity and expressiveness
• Title not available (Why is that?)
• Title not available (Why is that?)
• Real-Time Systems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Title not available (Why is that?)
• 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) and protocol specification, testing and verification (PSTV XVIII), Paris, France, November 3--6, 1998
• Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems

Cited In (5)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Three Approaches to Timed External Choice in UTP

Uses Software

• SPIN
• Uppaal

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)