scientific article; zbMATH DE number 15894
[For the entire collection see Zbl 0709.00020.] Concurrent systems are considered which are in fact finite collections of asynchronous interacting finite transition systems. The behavior of such a system CS is proposed to describe in terms of the propositional logic UB of branching time, with atomary propositions denoting states (or actions, in another interpretation ) of components of CS. There are two kinds of axioms. Axioms of the first kind (corresponding to transition relations of components of CS) refer to local times of components and define possible next states for (current) states of components. Axioms of the second kind refer to the global time of CS and define some constraints on global states and possible execution paths of CS. Among these constraints are, f.e., \(\forall G(\neg(p\& q))\) (mutual exclusion of states \(p\) and \(q\)), \(\neg p\&\neq q\supset\forall X(\neg q)\) which expresses (taken as an axiom what is equivalent to its closure under \(\forall G\), but not by itself as it can be understood from the authors' comments) that if \(p\) and \(q\) are false in a global state then in all the execution paths \(p\) must become true before \(q\). Using these axioms the axioms of the first kind are translated to axioms referring to the global time of CS. The main theorem (given without proofs) asserts (as I understand it from the authors' rather vague formulation) that a formula of UB can be deduced from these axioms iff it is valid in a finite model effectively constructible from these axioms. In the second part of the paper an algorithm is described which checks satisfiability of formulas of UB in finite models. It is noted that the algorithm is implemented on a SUN-3 workstation.
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Proving Failure-Free Properties of Concurrent Systems Using Temporal Logic
- On using temporal logic for refinement and compositional verification of concurrent systems
- scientific article; zbMATH DE number 4081518
- scientific article; zbMATH DE number 4119598
- scientific article; zbMATH DE number 52331
- Temporal logics for concurrent recursive programs: satisfiability and model checking
- Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking
- Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems
- scientific article; zbMATH DE number 3932379
- Proving properties of continuous systems: Qualitative simulation and temporal logic
- Static analysis for state-space reductions preserving temporal logics
- UNITY and Büchi automata
- Proving Failure-Free Properties of Concurrent Systems Using Temporal Logic
- scientific article; zbMATH DE number 4081518 (Why is no real title available?)
- TTL : a formalism to describe local and global properties of distributed systems
- scientific article; zbMATH DE number 4001471 (Why is no real title available?)
- scientific article; zbMATH DE number 4119598 (Why is no real title available?)
- scientific article; zbMATH DE number 7311251 (Why is no real title available?)
- Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems
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 Q3972532)
