About: Modal Transition Systems: Composition and LTL Model Checking

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

About: Modal Transition Systems: Composition and LTL Model Checking 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) is a~well established formalism used for specification and for abstract interpretation. We consider its disjunctive extension (DMTS) and we provide algorithms showing that refinement problems for DMTS are not harder than in the case of MTS. There are two main results in the paper. Firstly, we identify an error in a~previous attempt at LTL model checking of MTS and provide algorithms for LTL model checking of MTS and DMTS. Moreover, we show how to apply this result to compositional verification and circumvent the general incompleteness of the MTS composition. Secondly, we give a~solution to the common implementation and conjunctive composition problems lowering the complexity from EXPTIME to PTIME. Modal transition systems (MTS) is a~well established formalism used for specification and for abstract interpretation. We consider its disjunctive extension (DMTS) and we provide algorithms showing that refinement problems for DMTS are not harder than in the case of MTS. There are two main results in the paper. Firstly, we identify an error in a~previous attempt at LTL model checking of MTS and provide algorithms for LTL model checking of MTS and DMTS. Moreover, we show how to apply this result to compositional verification and circumvent the general incompleteness of the MTS composition. Secondly, we give a~solution to the common implementation and conjunctive composition problems lowering the complexity from EXPTIME to PTIME. (en)
Title	Modal Transition Systems: Composition and LTL Model Checking Modal Transition Systems: Composition and LTL Model Checking (en)
skos:prefLabel	Modal Transition Systems: Composition and LTL Model Checking Modal Transition Systems: Composition and LTL Model Checking (en)
skos:notation	RIV/00216224:14330/11:00049982!RIV12-GA0-14330___
http://linked.open...avai/predkladatel	Fakulta informatiky
http://linked.open...avai/riv/aktivita	P S Z
http://linked.open...avai/riv/aktivity	P(GAP202/11/0312), P(GD102/09/H042), S, Z(MSM0021622419)
http://linked.open...vai/riv/dodaniDat	2012
http://linked.open...aciTvurceVysledku	Beneš, Nikola Černá, Ivana 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	212849
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/11:00049982
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	modal transition systems; model checking; refinement; conjunction (en)
http://linked.open.../riv/klicoveSlovo	refinement model checking modal transition systems conjunction
http://linked.open...ontrolniKodProRIV	[A02C6E9F545C]
http://linked.open...v/mistoKonaniAkce	Taipei, Taiwan
http://linked.open...i/riv/mistoVydani	Heidelberg Dordrecht London New York
http://linked.open...i/riv/nazevZdroje	ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	3 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...vavai/riv/projekt	Software Components in Embedded Systems: Development and Verification Mathematical and Engineering Approaches to Developing Reliable and Secure Concurrent and Distributed Computer Systems
http://linked.open...UplatneniVysledku	2011
http://linked.open...iv/tvurceVysledku	Beneš, Nikola Černá, Ivana Křetínský, Jan
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2011-01-01 (xsd:date)
http://linked.open...n/vavai/riv/zamer	Highly Parallel and Distributed Computing Systems
number of pages	15 (xsd:int)
http://purl.org/ne...btex#hasPublisher	Springer-Verlag
https://schema.org/isbn	978-3-642-24371-4
http://localhost/t...ganizacniJednotka	14330
is http://linked.open...avai/riv/vysledek of	Modal Transition Systems: Composition and LTL Model Checking Modal Transition Systems: Composition and LTL Model Checking

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, 117 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software