Specifying message passing and time-critical systems with temporal logic

DOI10.1007/3-540-56283-4zbMATH Open0806.68074OpenAlexW2112494651MaRDI QIDQ684564FDOQ684564

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

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

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)

Cited In (18)

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

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)