Concurrent logic games on partial orders
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 s...
| Main Author: | |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer Berlin Heidelberg
2011
|
| _version_ | 1797107979200233472 |
|---|---|
| author | Gutierrez, J |
| author_facet | Gutierrez, J |
| author_sort | Gutierrez, J |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T07:23:04Z |
| format | Conference item |
| id | oxford-uuid:8d5b5021-7e16-4c01-9aa9-231a48ac7c55 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T07:23:04Z |
| publishDate | 2011 |
| publisher | Springer Berlin Heidelberg |
| record_format | dspace |
| spelling | oxford-uuid:8d5b5021-7e16-4c01-9aa9-231a48ac7c552022-10-28T12:04:43ZConcurrent logic games on partial ordersConference itemhttp://purl.org/coar/resource_type/c_5794uuid:8d5b5021-7e16-4c01-9aa9-231a48ac7c55EnglishSymplectic Elements at OxfordSpringer Berlin Heidelberg2011Gutierrez, JMost 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. |
| spellingShingle | Gutierrez, J Concurrent logic games on partial orders |
| title | Concurrent logic games on partial orders |
| title_full | Concurrent logic games on partial orders |
| title_fullStr | Concurrent logic games on partial orders |
| title_full_unstemmed | Concurrent logic games on partial orders |
| title_short | Concurrent logic games on partial orders |
| title_sort | concurrent logic games on partial orders |
| work_keys_str_mv | AT gutierrezj concurrentlogicgamesonpartialorders |