BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN and Jiří SRBA. Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete. In Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings. Heidelberg: Springer-Verlag, 2009. p. 112-126. ISBN 978-3-642-03465-7. doi:10.1007/978-3-642-03466-4_7.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete
Name in Czech Zevrubné zjemnění na modálních přechodových systémech je EXPTIME-úplný problém
Authors BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Jan KŘETÍNSKÝ (203 Czech Republic, guarantor, belonging to the institution), Kim G. LARSEN (208 Denmark) and Jiří SRBA (203 Czech Republic, belonging to the institution).
Edition Heidelberg, Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings, p. 112-126, 15 pp. 2009.
Publisher Springer-Verlag
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Malaysia
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/09:00065771
Organization unit Faculty of Informatics
ISBN 978-3-642-03465-7
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-642-03466-4_7
UT WoS 000269931000007
Keywords in English compositional verification; modal transition systems; refinement
Tags compositional verification, modal transition systems, REFINEMENT
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 30/4/2014 05:53.
Abstract
Modal transition systems (MTS), a specification formalism introduced more than 20 years ago, has recently received a considerable attention in several different areas. Many of the fundamental questions related to MTSs have already been answered. However, the problem of the exact computational complexity of thorough refinement checking between two finite MTSs remained unsolved and was repeatedly stated as an open problem. We settle down this question by showing EXPTIME-completeness of thorough refinement checking on finite MTSs. The upper-bound result relies on a novel algorithm running in single exponential time providing a direct goal-oriented way to decide thorough refinement. If the right-hand side MTS is moreover deterministic, or has a fixed size, the running time of the algorithm becomes polynomial. The lower-bound proof is achieved by reduction from the acceptance problem of alternating linear bounded automata and the problem remains EXPTIME-hard even if the left-hand side MTS is fixed.
Abstract (in Czech)
Modální přechodové systémy (MTS), specifikační formalismus zavedený před více než 20 lety, jsou nyní ve středu zájmů v řadě různých oblastí. Mnoho základních otázek o MTS již bylo zodpovězeno. Nicméně otázka přesné složitosti zevrubného zjemnění mezi dvěma konečnými MTS zůstala otevřená a byla opakována jako otevřený problém. Tuto otázku zodpovídáme důkazem EXPTIME-úplnosti tohoto problému. Horního odhadu je docíleno exponenciálním algoritmem. Navíc pokud je pravá strana deterministická nebo fixovaná, algoritmus se stává polynomiálním. Dolní odhad je dokázán redukcí z problému akceptace alternujícího lineáně ohraničeného automatu a problém zůstává EXPTIME-těžký, i pokud je levá strana fixována.
Links
MSM0021622419, plan (intention)Name: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
1ET408050503, research and development projectName: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems
1M0545, research and development projectName: Institut Teoretické Informatiky
Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science
PrintDisplayed: 28/11/2022 23:23