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

Decidability, Behavioural Equivalences and Infinite Transition Graphs

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

รายละเอียด

ชื่อเรื่อง : Decidability, Behavioural Equivalences and Infinite Transition Graphs
นักวิจัย : Hüttel, Hans
คำค้น : -
หน่วยงาน : Edinburgh Research Archive, United Kingdom
ผู้ร่วมงาน : Stirling, Colin
ปีพิมพ์ : 2534
อ้างอิง : http://hdl.handle.net/1842/411
ที่มา : -
ความเชี่ยวชาญ : -
ความสัมพันธ์ : -
ขอบเขตของเนื้อหา : -
บทคัดย่อ/คำอธิบาย :

This thesis studies behavioural equivalences on labelled infinite transition graphs and the role that they can play in the context of modal logics and notions from language theory. A natural class of such infinite graphs is that corresponding to the SnS-definable tree languages first studied by Rabin. We show that a modal mu-calculus with label set {0,...,n - 1} can define these tree languages up to an observational equivalence. Another natural class of infinite transition graphs is that of normed BPA processes, which correspond to the graphs of leftmost derivations in context-free grammars without useless productions. A remarkable result is that strong bisimulation is decidable for these graphs. After an outline of the existing proofs due to Baeten et al. and Caucal we present a much simpler proof using a tableau system closely related to the branching algorithms employed in language theory following Korenjak and Hopcroft. We then present a result due to Colin Stirling, giving a weakly sound and complete sequent-based equational theory for bisimulation equivalence for normed BPA processes from the tableau system. Moreover, we show how to extract a fundamental relation (as in the work of Caucal) from a successful tableau. We then introduce silent actions and consider a class of normed BPA processes with the restriction that processes cannot terminate silently, showing that the decidability result for strong bisimilarity can be extended to van Glabbeek's branching bisimulation equivalence for this class of processes. We complete the picture by establishing that all other known behavioural equivalences and a number of preorders are undecidable for normed BPA processes.

บรรณานุกรม :
Hüttel, Hans . (2534). Decidability, Behavioural Equivalences and Infinite Transition Graphs.
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom .
Hüttel, Hans . 2534. "Decidability, Behavioural Equivalences and Infinite Transition Graphs".
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom .
Hüttel, Hans . "Decidability, Behavioural Equivalences and Infinite Transition Graphs."
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom , 2534. Print.
Hüttel, Hans . Decidability, Behavioural Equivalences and Infinite Transition Graphs. กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom ; 2534.