scientific article; zbMATH DE number 4119617
From MaRDI portal
Publication:4733399
zbMath0683.68031MaRDI QIDQ4733399
Publication date: 1989
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Artificial intelligence (68T99) Theory of operating systems (68N25) Temporal logic (03B44)
Related Items (29)
Logics and decidability for labelled pre- and partially ordered Kripke structures ⋮ Specification and verification of decentralized daisy chain arbiters with \(\omega\)-extended regular expressions ⋮ A compositional framework for fault tolerance by specification transformation ⋮ Application of the composition principle to unity-like specifications ⋮ Deontic action logic, atomic Boolean algebras and fault-tolerance ⋮ Specification of abstract dynamic-data types: A temporal logic approach ⋮ Towards better heuristics for solving bounded model checking problems ⋮ Representing regular languages of infinite words using mod 2 multiplicity automata ⋮ A computer scientist looks at game theory. ⋮ Automated analysis of mutual exclusion algorithms using CCS ⋮ Completing the temporal picture ⋮ Temporal logic and categories of Petri nets ⋮ Reasoning about programs by exploiting the environment ⋮ Model checking properties on reduced trace systems ⋮ A hierarchy of temporal logics with past ⋮ On using temporal logic for refinement and compositional verification of concurrent systems ⋮ Local model checking for infinite state spaces ⋮ On undecidability of propositional temporal logics on trace systems ⋮ Automatic verification of distributed systems: the process algebra approach. ⋮ Modal logics for communicating systems ⋮ Axioms for real-time logics ⋮ Decision Procedures for a Deontic Logic Modeling Temporal Inheritance of Obligations ⋮ Reasoning about nondeterministic and concurrent actions: A process algebra approach ⋮ Verification of reactive systems using temporal logic with clocks ⋮ Simulation, reduction and preservation of correctness properties of parallel systems ⋮ Specification in CTL + past for verification in CTL. ⋮ Testing preorders for probabilistic processes can be characterized by simulations ⋮ On the strength of temporal proofs ⋮ Proving partial order properties
This page was built for publication: