Concurrent logic games on partial orders

Conference item

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.

Authors: Gutierrez, J

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Springer Berlin Heidelberg
• Host title: Logic, Language, Information and Computation. WoLLIC 2011
• Pages: 146-160
• Series: Lecture Notes in Computer Science
• Series number: 6642
• Publication date: 2011-04-28
• Event title: 18th Workshop on Logic, Language, Information and Computation (WoLLIC 2011)
• Event location: Philadelphia, PA, USA
• Event start date: 2011-05-18
• Event end date: 2011-05-20
• DOI: 10.1007/978-3-642-20920-8_17
• ISSN: 1611-3349
• EISBN: 978-3-642-20920-8
• ISBN: 978-3-642-20919-2
• Language: English
• Keywords: winning strategy; closure operator; local strategy; partial order; local position