scientific article

zbMath0765.68121MaRDI QIDQ4037378

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

Publication date: 18 May 1993

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

correctnessmodel checkingtemporal logicsatisfiabilitydistributed programsreal-time programsreal-time computation tree logic

Mathematics Subject Classification ID

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

Related Items (20)

Nondeterministic probabilistic Petri net -- a new method to study qualitative and quantitative behaviors of system ⋮ A new model for model checking: cycle-weighted Kripke structure ⋮ Verifying Real-Time Properties of Multi-agent Systems via SMT-Based Bounded Model Checking ⋮ On the expressivity and complexity of quantitative branching-time temporal logics ⋮ Processing disjunctions in temporal constraint networks ⋮ Branching vs. Linear Time: Semantical Perspective ⋮ A space-efficient on-the-fly algorithm for real-time model checking ⋮ Semantics of temporal constrained objects ⋮ Min-max Computation Tree Logic ⋮ Meanings of Model Checking ⋮ A real-time interval logic and its decision procedure ⋮ What good are digital clocks? ⋮ Time-budgeting: a component based development methodology for real-time embedded systems ⋮ Unnamed Item ⋮ From liveness to promptness ⋮ Verification of reactive systems using temporal logic with clocks ⋮ The Verus language: Representing time efficiently with BDDs ⋮ Quantitative \(\mu\)-calculus and CTL defined over constraint semirings ⋮ Collecting statistics over runtime executions ⋮ A theory of timed automata

This page was built for publication: