An action-based framework for veryfying logical and behavioural properties of concurrent systems

DOI10.1016/0169-7552(93)90047-8zbMath0789.68096OpenAlexW2025788721MaRDI QIDQ4697197

Rocco De Nicola, Gioia Ristori, Alessandro Fantechi, Stefania Gnesi

Publication date: 29 June 1993

Published in: Computer Networks and ISDN Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0169-7552(93)90047-8

zbMATH Keywords

concurrent systemsprocess algebratemporal logicbehavioural equivalenceslabelled transition systemformal description techniquesbranching time logicverification environments

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (12)

Model checking for action-based logics ⋮ Assisting requirement formalization by means of natural language translation ⋮ Model checking mobile ad hoc networks ⋮ ACTL for modal interface automata ⋮ Compositional Specification in Rewriting Logic ⋮ Compositionality and bisimulation: A negative result ⋮ ACTLW -- an action-based computation tree logic with unless operator ⋮ Automatic verification of distributed systems: the process algebra approach. ⋮ Model checking fuzzy computation tree logic ⋮ Folk Theorems on the Correspondence between State-Based and Event-Based Systems ⋮ Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking ⋮ Compositional verification of asynchronous concurrent systems using CADP

Uses Software

• AUTO

This page was built for publication: An action-based framework for veryfying logical and behavioural properties of concurrent systems