ridm@nrct.go.th   ระบบคลังข้อมูลงานวิจัยไทย   รายการโปรดที่คุณเลือกไว้

On bisimulation and model-checking for concurrent systems with partial order semantics

หน่วยงาน Edinburgh Research Archive, United Kingdom

รายละเอียด

ชื่อเรื่อง : On bisimulation and model-checking for concurrent systems with partial order semantics
นักวิจัย : Gutierrez, Julian
คำค้น : mathematical logic , true concurrency , infinite games , fixpoint modal logics
หน่วยงาน : Edinburgh Research Archive, United Kingdom
ผู้ร่วมงาน : Bradfield, Julian , Stark, Ian , Stirling, Colin , Engineering and Physical Sciences Research Council (EPSRC)
ปีพิมพ์ : 2554
อ้างอิง : http://hdl.handle.net/1842/5281
ที่มา : -
ความเชี่ยวชาญ : -
ความสัมพันธ์ : Gutierrez, J.: Logics and bisimulation games for concurrency, causality and conflict. In: FOSSACS. LNCS 5504, 48–62, Springer (2009) , Gutierrez, J.: Logics and games for true concurrency. Informatics Report Series, Technical Report EDI-INF-RR-1393, University of Edinburgh (2010) , Gutierrez, J.: Concurrent logic games on partial orders. In: WoLLIC. LNCS 6642, 146-160, Springer (2011) , Gutierrez, J., Bradfield, J.C.: Model-checking games for fixpoint logics with partial order models. In: CONCUR. LNCS 5710, 354–368, Springer (2009) , Gutierrez, J., Bradfield, J.C.: Model-checking games for fixpoint logics with partial order models. Information and Computation 209(5), 766–781 (2011)
ขอบเขตของเนื้อหา : -
บทคัดย่อ/คำอธิบาย :

EP/G012962/1

In concurrency theory—the branch of (theoretical) computer science that studies the logical and mathematical foundations of parallel computation—there are two main formal ways of modelling the behaviour of systems where multiple actions or events can happen independently and at the same time: either with interleaving or with partial order semantics. On the one hand, the interleaving semantics approach proposes to reduce concurrency to the nondeterministic, sequential computation of the events the system can perform independently. On the other hand, partial order semantics represent concurrency explicitly by means of an independence relation on the set of events that the system can execute in parallel; following this approach, the so-called ‘true concurrency’ approach, independence or concurrency is a primitive notion rather than a derived concept as in the interleaving framework. Using interleaving or partial order semantics is, however, more than a matter of taste. In fact, choosing one kind of semantics over the other can have important implications—both from theoretical and practical viewpoints—as making such a choice can raise different issues, some of which we investigate here. More specifically, this thesis studies concurrent systems with partial order semantics and focuses on their bisimulation and model-checking problems; the theories and techniques herein apply, in a uniform way, to different classes of Petri nets, event structures, and transition system with independence (TSI) models. Some results of this work are: a number of mu-calculi (in this case, fixpoint extensions of modal logic) that, in certain classes of systems, induce exactly the same identifications as some of the standard bisimulation equivalences used in concurrency. Secondly, the introduction of (infinite) higher-order logic games for bisimulation and for model-checking, where the players of the games are given (local) monadic second-order power on the sets of elements they are allowed to play. And, finally, the formalization of a new order-theoretic concurrent game model that provides a uniform approach to bisimulation and model-checking and bridges some mathematical concepts in order theory with the more operational world of games. In particular, we show that in all cases the logic games for bisimulation and model-checking developed in this thesis are sound and complete, and therefore, also determined—even when considering models of infinite state systems; moreover, these logic games are decidable in the finite case and underpin novel decision procedures for systems verification. Since the mu-calculi and (infinite) logic games studied here generalise well-known fixpoint modal logics as well as game-theoretic decision procedures for analysing concurrent systems with interleaving semantics, this thesis provides some of the groundwork for the design of a logic-based, game-theoretic framework for studying, in a uniform manner, several concurrent systems regardless of whether they have an interleaving or a partial order semantics.

บรรณานุกรม :
Gutierrez, Julian . (2554). On bisimulation and model-checking for concurrent systems with partial order semantics.
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom .
Gutierrez, Julian . 2554. "On bisimulation and model-checking for concurrent systems with partial order semantics".
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom .
Gutierrez, Julian . "On bisimulation and model-checking for concurrent systems with partial order semantics."
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom , 2554. Print.
Gutierrez, Julian . On bisimulation and model-checking for concurrent systems with partial order semantics. กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom ; 2554.