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

DOI10.1016/0169-7552(93)90047-8zbMATH Open0789.68096OpenAlexW2025788721MaRDI QIDQ4697197FDOQ4697197

Rocco De Nicola, Gioia Ristori, Alessandro Fantechi, S. 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

Recommendations

• Model checking for action-based logics
• scientific article; zbMATH DE number 4128366
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• scientific article; zbMATH DE number 5181778
• ACTLW -- an action-based computation tree logic with unless operator

zbMATH Keywords

process algebratemporal logicformal description techniquesbehavioural equivalencesconcurrent systemslabelled transition systembranching 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)

Cited In (16)

• Automatic verification of distributed systems: the process algebra approach.
• ACTLW -- an action-based computation tree logic with unless operator
• Folk Theorems on the Correspondence between State-Based and Event-Based Systems
• Model checking for action-based logics
• Towards the assessment of logics for concurrent actions
• ACTL for modal interface automata
• Verification and refinement with fine-grained action-based concurrent objects
• Title not available (Why is that?)
• Assisting requirement formalization by means of natural language translation
• Compositional Specification in Rewriting Logic
• Encoding safety in \(\mathrm{CLL}_R\)
• Compositional verification of asynchronous concurrent systems using CADP
• Compositionality and bisimulation: A negative result
• Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking
• Model checking mobile ad hoc networks
• Model checking fuzzy computation tree logic

Uses Software

• AUTO

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4697197)