ACTLW -- an action-based computation tree logic with unless operator

DOI10.1016/j.ins.2007.10.023zbMath1134.68033MaRDI QIDQ2476788

Tatjana Kapus, Robert Meolic, Zmago Brezočnik

Publication date: 12 March 2008

Published in: Information Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ins.2007.10.023

zbMATH Keywords

fixed point; formal verification; model checking; action-based temporal logic; mutual-exclusion algorithm

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

03B44: Temporal logic

Related Items

ACTLW, Modal transition systems with weight intervals, A state/event-based model-checking approach for the analysis of abstract system properties, An accessible verification environment for UML models of services, ACTLW -- an action-based computation tree logic with unless operator, Model Checking Value-Passing Modal Specifications

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automated analysis of mutual exclusion algorithms using CCS
• Symbolic model checking: \(10^{20}\) states and beyond
• Model checking for action-based logics
• ACTLW -- an action-based computation tree logic with unless operator
• Standards and verification for fair-exchange and atomicity in e-commerce transactions
• Algebraic laws for nondeterminism and concurrency
• An action-based framework for veryfying logical and behavioural properties of concurrent systems
• Checking a Mutex Algorithm in a Process Algebra with Fairness