Model checking for action-based logics

DOI10.1007/BF01384084zbMath0804.68086MaRDI QIDQ1326587

Gioia Ristori, Alessandro Fantechi, Stefania Gnesi

Publication date: 19 June 1994

Published in: Formal Methods in System Design (Search for Journal in Brave)

zbMATH Keywords

concurrent systemsmodel checkingabstract specificationsaction-based logics

Mathematics Subject Classification ID

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

Related Items (5)

Quantitative Analysis of Communication Scenarios ⋮ ACTLW -- an action-based computation tree logic with unless operator ⋮ Model checking fuzzy computation tree logic ⋮ 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

Cites Work

• Unnamed Item
• Proof systems for satisfiability in Hennessy-Milner logic with recursion
• Calculi for synchrony and asynchrony
• Characterizing finite Kripke structures in propositional temporal logic
• A calculus of communicating systems
• Symbolic model checking: \(10^{20}\) states and beyond
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• “Sometimes” and “not never” revisited
• Algebraic laws for nondeterminism and concurrency
• An action-based framework for veryfying logical and behavioural properties of concurrent systems

This page was built for publication: Model checking for action-based logics