Concurrent logic games on partial orders

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

8 Citations (Scopus)


Most games for analysing concurrent systems are played on interleaving models, such as graphs or infinite trees. However, several concurrent systems have partial order models rather than interleaving ones. As a consequence, a potentially algorithmically undesirable translation from a partial order setting to an interleaving one is required before analysing them with traditional techniques. In order to address this problem, this paper studies a game played directly on partial orders and describes some of its algorithmic applications. The game provides a unified approach to system and property verification which applies to different decision problems and models of concurrency. Since this framework uses partial orders to give a uniform representation of concurrent systems, logical specifications, and problem descriptions, it is particularly suitable for reasoning about concurrent systems with partial order semantics, such as Petri nets or event structures. Two applications can be cast within this unified approach: bisimulation and model-checking.

Original languageEnglish
Title of host publicationLogic, Language, Information and Computation - 18th International Workshop, WoLLIC 2011, Proceedings
Number of pages15
ISBN (Print)9783642209192
Publication statusPublished - 2011
Externally publishedYes

Publication series

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

Cite this