Games and Logics with Partial Order Models

Julian Gutierrez ( University of Edinburgh )

Concurrency theory is concerned with the logical and mathematical study of parallel processes, i.e., of systems composed of a number of independent components which interact with each other and with an environment. These systems can be analysed by studying the logical formalisms employed to specify and verify their properties as well as the mathematical structures used to represent their behaviour. Such structures can be of two different kinds: interleaving or partially ordered. As a consequence, theories, tools and techniques for studying concurrent systems have to take this difference into account. However, most theoretical developments have been done considering the interleaving representations. We study logics and verification techniques for systems with partial order models of concurrency. In particular, using a game-theoretic approach, we study fixpoint modal logics with partial order models of concurrency and their associated bisimulation and model-checking problems. Our research extends previous studies for interleaving concurrency, while achieving new results for partial order models.