Files in this item

FilesDescriptionFormat

application/pdf

application/pdfidealsTechRep.pdf (455kB)
Updated file January 31 2011PDF

Description

Title:State/Event-based LTL Model Checking under Parametric Generalized Fairness
Author(s):Bae, Kyungmin; Meseguer, José
Subject(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.
Issue Date:2010-01-29
Genre:Article
Type:Text
Language:English
URI:http://hdl.handle.net/2142/18654
Publication Status:unpublished
Date Available in IDEALS:2011-01-29


This item appears in the following Collection(s)

Item Statistics