About: EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems

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

About: EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems 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. 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 and deterministic. 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. 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 and deterministic. (en)
Title	EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems (en)
skos:prefLabel	EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems (en)
skos:notation	RIV/00216224:14330/12:00057563!RIV13-GA0-14330___
http://linked.open...avai/riv/aktivita	I P S
http://linked.open...avai/riv/aktivity	I, P(GAP202/10/1469), P(GAP202/11/0312), S
http://linked.open...iv/cisloPeriodika	September
http://linked.open...vai/riv/dodaniDat	2013
http://linked.open...aciTvurceVysledku	Srba, Jiří Beneš, Nikola Křetínský, Jan
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
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	135892
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/12:00057563
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	modal transition systems; refinement; computational complexity (en)
http://linked.open.../riv/klicoveSlovo	refinement computational complexity modal transition systems
http://linked.open...odStatuVydavatele	NL - Nizozemsko
http://linked.open...ontrolniKodProRIV	[6D95719E7A52]
http://linked.open...i/riv/nazevZdroje	Information and Computation
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	Formal methods for analysis and verification of complex systems Software Components in Embedded Systems: Development and Verification
http://linked.open...UplatneniVysledku	2012
http://linked.open...v/svazekPeriodika	218
http://linked.open...iv/tvurceVysledku	Beneš, Nikola Larsen, Kim G. Srba, Jiří Křetínský, Jan
http://linked.open...ain/vavai/riv/wos	000309195100004
issn	0890-5401
number of pages	15 (xsd:int)
http://bibframe.org/vocab/doi	10.1016/j.ic.2012.08.001
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, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software