Specifying message passing and time-critical systems with temporal logic

DOI10.1007/3-540-56283-4MaRDI QIDQ684564zbMATHOpenAlexFDO

Authors Ron Koymans

Publication date 20 September 1993

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://research.tue.nl/nl/publications/specifying-message-passing-and-timecritical-systems-with-temporal-logic(55a75f5e-43b9-483c-ab3e-8b206d56d515).html

zbMATH Keywords

specificationtemporal logicmessage passing systemsmulti-modal logictime-critical systems

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 4089533
• Temporal logic in specification. Altrincham, UK, April 8-10, 1987. Proceedings
• scientific article; zbMATH DE number 52331
• scientific article; zbMATH DE number 218548
• A really temporal logic

Cited in

(18)

• Linear-time temporal logic with event freezing functions
• scientific article; zbMATH DE number 1953036 (Why is no real title available?)
• Early verification and validation of mission critical systems
• Metric temporal logic with durations
• Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application
• Can message buffers be axiomatized in linear temporal logic?
• Compositional verification of real-time systems with explicit clock temporal logic
• Decidability results for metric and layered temporal logics
• Duration calculus: Logical foundations
• scientific article; zbMATH DE number 4112564 (Why is no real title available?)
• A hybridization of irreflexive modal logics
• Programming in metric temporal logic
• Inequality without irreflexivity
• scientific article; zbMATH DE number 4089533 (Why is no real title available?)
• Axioms for real-time logics
• Formalization of invariant patterns for the invariant refinement method
• Reasoning about layered message passing systems
• SMT-based satisfiability of first-order LTL with event freezing functions and metric operators

This page was built for publication: Specifying message passing and time-critical systems with temporal logic

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