scientific article; zbMATH DE number 177509

MaRDI QIDQ4037378zbMATH OpenFDO

Authors Aloysius K. Mok, A. P. Sistla, Jai Srinivasan, E. Allen Emerson

Publication date 18 May 1993

zbMATH Keywords

correctnessdistributed programsmodel checkingreal-time computation tree logicreal-time programssatisfiabilitytemporal logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Symbolic model checking for real-time systems
• A really temporal logic
• scientific article; zbMATH DE number 176728
• scientific article; zbMATH DE number 4128370
• Model-checking in dense real-time

Cited in

(37)

• From liveness to promptness
• Reasoning in a restricted temporal logic
• A theory of timed automata
• Symbolic model checking for real-time systems
• Extending Hoare logic to real-time
• On the expressivity and complexity of quantitative branching-time temporal logics
• Processing disjunctions in temporal constraint networks
• Verification of reactive systems using temporal logic with clocks
• The Verus language: Representing time efficiently with BDDs
• A branching time temporal framework for quantitative reasoning
• Semantics of temporal constrained objects
• Synthesis for continuous time
• Quantitative \(\mu\)-calculus and CTL defined over constraint semirings
• Nondeterministic probabilistic Petri net -- a new method to study qualitative and quantitative behaviors of system
• scientific article; zbMATH DE number 5916930 (Why is no real title available?)
• scientific article; zbMATH DE number 3868590 (Why is no real title available?)
• Branching vs. Linear Time: Semantical Perspective
• A new model for model checking: cycle-weighted Kripke structure
• Branching-Time Property Preservation Between Real-Time Systems
• scientific article; zbMATH DE number 4128370 (Why is no real title available?)
• Verifying real-time properties of multi-agent systems via SMT-based bounded model checking
• scientific article; zbMATH DE number 1852150 (Why is no real title available?)
• Timed network games
• Meanings of model checking
• What good are digital clocks?
• Algebraic Methodology and Software Technology
• Verifying RTECTL properties of a train controller systems
• Synthesis for temporal logic over the reals
• Computational Logic in Multi-Agent Systems
• Translating a continuous-time temporal logic into timed automata.
• Min-max Computation Tree Logic
• A real-time interval logic and its decision procedure
• A space-efficient on-the-fly algorithm for real-time model checking
• Development of safety-critical real-time systems
• Reasoning with numeric and symbolic time information
• Time-budgeting: a component based development methodology for real-time embedded systems
• Collecting statistics over runtime executions

This page was built for publication:

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