scientific article

Rajeev Alur, David L. Dill, Costas Courcoubetis

Publication date: 18 May 1993

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

model-checking verification of concurrent systems branching-time temporal logic generalized semi-Markov processes finite-state discrete-time Markov chains stochastic real-time systems

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Efficient timed model checking for discrete-time systems, Language Emptiness of Continuous-Time Parametric Timed Automata, Performance Evaluation of Schedulers in a Probabilistic Setting, A logic for reasoning about time and reliability, An iterative approach to verification of real-time systems, Model-checking discrete duration calculus, Model-checking for real-time systems, Time-Bounded Verification, Strict Divergence for Probabilistic Timed Automata, A calculus of stochastic systems for the specification, simulation, and hidden state estimation of mixed stochastic/nonstochastic systems, A new model for model checking: cycle-weighted Kripke structure, Symbolic model checking for probabilistic processes, Duration calculus: Logical foundations, Temporal Specifications with Accumulative Values, Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems, A survey of timed automata for the development of real-time systems, On the expressivity and complexity of quantitative branching-time temporal logics, On Caputo-Hadamard type fractional impulsive hybrid systems with nonlinear fractional integral conditions, Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms, Cyber-physical systems, Superposition as a decision procedure for timed automata, Model checking time-dependent system specifications using time stream Petri nets and \texttt{UPPAAL}, Verification of duration systems using an approximation approach, Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions, Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains, Deciding properties of integral relational automata, Automatic synthesis of real time systems, Modular abstractions for verifying real-time distributed systems, Minimum and maximum delay problems in real-time systems, Specification and automatic verification of self-timed queues, Model checking for probabilistic timed automata, Bayesian statistical model checking with application to Stateflow/Simulink verification, Using mappings to prove timing properties, On impulsive boundary value problems of fractional differential equations with irregular boundary conditions, The well-designed logical robot: learning and experience from observations to the Situation Calculus, A menagerie of timed automata, Ensuring completeness of symbolic verification methods for infinite-state systems, On the expressiveness of TPTL and MTL, Statistical probabilistic model checking with a focus on time-bounded properties, Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata, Probabilistic and Topological Semantics for Timed Automata, Symbolic Branching Bisimulation-Checking of Dense-Time Systems in an Environment, Fixed-Delay Events in Generalized Semi-Markov Processes Revisited, Verifying automata specification of distributed probabilistic real-time systems, Model-checking Timed Temporal Logics, Verification of continuous dynamical systems by timed automata, Information system design of manufacturing environments, TPAP, Probabilistic temporal logics via the modal mu-calculus, A note on the attractor-property of infinite-state Markov chains, On a class of timer hybrid systems reducible to finite state automata, PLC-automata: A new class of implementable real-time automata, A theory of stochastic systems. I: Stochastic automata, Model checking of systems with many identical timed processes, Calculating Probabilities of Real-Time Test Cases, On the verification of qualitative properties of probabilistic processes under fairness constraints., A maximal entropy stochastic process for a timed automaton, Automatic verification of real-time systems with discrete probability distributions., Undecidable verification problems for programs with unreliable channels, Formal analysis and control of timed automata with guards using (max, +) and (min, +) algebras, A theory of timed automata, From ATP to timed graphs and hybrid systems, Checking timed Büchi automata emptiness efficiently, A supervisory control method for ensuring the conformance of real-time discrete event systems, Uniformity for the decidability of hybrid automata