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

Inclusion problems for one-counter systems

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

รายละเอียด

ชื่อเรื่อง : Inclusion problems for one-counter systems
นักวิจัย : Totzke, Patrick
คำค้น : infinite-state systems , verification problems , one-counter automata , decidability , deterministic processes
หน่วยงาน : Edinburgh Research Archive, United Kingdom
ผู้ร่วมงาน : Mayr, Richard , Stirling, Colin , Engineering and Physical Sciences Research Council (EPSRC) , SICSA , LFCS
ปีพิมพ์ : 2557
อ้างอิง : http://hdl.handle.net/1842/9646
ที่มา : -
ความเชี่ยวชาญ : -
ความสัมพันธ์ : P. A. Abdulla, M. F. Atig, P. Hofman, R. Mayr, K. N. Kumar, and P. Totzke. “Infinite- State Energy Games”. In: LICS. 2014. , P. Hofman, S. Lasota, R. Mayr, and P. Totzke. “Simulation Over One-Counter Nets is PSPACE-Complete”. In: FSTTCS. 2013, pp. 515–526. , P. Hofman, R. Mayr, and P. Totzke. “Decidability of Weak Simulation on One-Counter Nets”. In: LICS. 2013, pp. 203–212.
ขอบเขตของเนื้อหา : -
บทคัดย่อ/คำอธิบาย :

We study the decidability and complexity of verification problems for infinite-state systems. A fundamental question in formal verification is if the behaviour of one process is reproducible by another. This inclusion problem can be studied for various models of computation and behavioural preorders. It is generally intractable or even undecidable already for very limited computational models. The aim of this work is to clarify the status of the decidability and complexity of some well-known inclusion problems for suitably restricted computational models. In particular, we address the problems of checking strong and weak simulation and trace inclusion for processes definable by one-counter automata (OCA), that consist of a finite control and a single counter ranging over the non-negative integers. We take special interest of the subclass of one-counter nets (OCNs), that cannot fully test the counter for zero and which is subsumed both by pushdown automata and Petri nets / vector addition systems. Our new results include the PSPACE-completeness of strong and weak simulation, and the undecidability of trace inclusion for OCNs. Moreover, we consider semantic preorders between OCA/OCN and finite systems and close some gaps regarding their complexity. Finally, we study deterministic processes, for which simulation and trace inclusion coincide.

บรรณานุกรม :
Totzke, Patrick . (2557). Inclusion problems for one-counter systems.
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom .
Totzke, Patrick . 2557. "Inclusion problems for one-counter systems".
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom .
Totzke, Patrick . "Inclusion problems for one-counter systems."
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom , 2557. Print.
Totzke, Patrick . Inclusion problems for one-counter systems. กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom ; 2557.