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

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