State/event-based LTL model checking under parametric generalized fairness

Kyungmin Bae, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 as well as an on-the-fly model checking algorithm to verify LTL properties under universally quantified parametric fairness assumptions, specified by generalized strong/weak fairness formulas. 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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 23rd International Conference, CAV 2011, Proceedings
Number of pages17
StatePublished - 2011
Event23rd International Conference on Computer Aided Verification, CAV 2011 - Snowbird, UT, United States
Duration: Jul 14 2011Jul 20 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6806 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other23rd International Conference on Computer Aided Verification, CAV 2011
Country/TerritoryUnited States
CitySnowbird, UT


  • Model checking
  • Parameterized Fairness
  • State/Event LTL

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'State/event-based LTL model checking under parametric generalized fairness'. Together they form a unique fingerprint.

Cite this