State/Event-based LTL Model Checking under Parametric Generalized Fairness

Bae, Kyungmin; Meseguer, José

Permalink

https://hdl.handle.net/2142/18654 Copy

Description

Title

State/Event-based LTL Model Checking under Parametric Generalized Fairness

Author(s)

• Bae, Kyungmin
• Meseguer, José

Issue Date

2010-01-29

Keyword(s)

• Model checking
• Fairness
• Localized Fairness
• State/Event LTL
• Parametrization

Abstract

In modeling a concurrent system, fairness constraints are usually considered at a specific granularity level of the system, leading to many different variants of fairness: transition fairness, object/process fairness, actor fairness, etc. These different notions of fairness can be unified by making explicit their parametrization over the relevant entities in the system as universal quantification. We propose a state/event-based framework to verify LTL properties under parametric fairness, specified by generalized strong/weak fairness formulas. We also present an on-the-fly automata-based algorithm for model checking LTL formulas under universally quantified parameterized fairness assumptions. It enables verification of temporal properties under fairness conditions associated to dynamic entities such as new process creations. We have implemented our algorithm within the Maude system.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/18654

Owning Collections