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

DOI10.1016/j.ins.2007.10.023zbMath1134.68033OpenAlexW2061609623MaRDI 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 pointformal verificationmodel checkingaction-based temporal logicmutual-exclusion algorithm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (8)

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

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

This page was built for publication: ACTLW -- an action-based computation tree logic with unless operator