About: Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
Description	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. 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. (en)
Title	Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete (en)
skos:prefLabel	Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete (en)
skos:notation	RIV/00216224:14330/09:00065771!RIV14-MSM-14330___
http://linked.open...avai/riv/aktivita	P S Z
http://linked.open...avai/riv/aktivity	P(1ET408050503), P(1M0545), S, Z(MSM0021622419)
http://linked.open...vai/riv/dodaniDat	2014
http://linked.open...aciTvurceVysledku	Srba, Jiří Beneš, Nikola Křetínský, Jan
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Masarykova univerzita / Fakulta informatiky
http://linked.open...dnocenehoVysledku	306867
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/09:00065771
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	compositional verification; modal transition systems; refinement (en)
http://linked.open.../riv/klicoveSlovo	refinement modal transition systems compositional verification
http://linked.open...ontrolniKodProRIV	[87FDC05595FF]
http://linked.open...v/mistoKonaniAkce	Kuala Lumpur
http://linked.open...i/riv/mistoVydani	Heidelberg
http://linked.open...i/riv/nazevZdroje	Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	3 (xsd:int)
http://linked.open...cetTvurcuVysledku	4 (xsd:int)
http://linked.open...vavai/riv/projekt	Institute for Theoretical Computer Science Techniques for automatic verification and validation of software and hardware systems
http://linked.open...UplatneniVysledku	2009
http://linked.open...iv/tvurceVysledku	Beneš, Nikola Larsen, Kim G. Srba, Jiří Křetínský, Jan
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open...ain/vavai/riv/wos	000269931000007
http://linked.open.../riv/zahajeniAkce	2009-01-01 (xsd:date)
http://linked.open...n/vavai/riv/zamer	Highly Parallel and Distributed Computing Systems
issn	0302-9743
number of pages	15 (xsd:int)
http://bibframe.org/vocab/doi	10.1007/978-3-642-03466-4_7
http://purl.org/ne...btex#hasPublisher	Springer-Verlag
https://schema.org/isbn	9783642034657
http://localhost/t...ganizacniJednotka	14330

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 112 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software