D 2013

On Refinements of Boolean and Parametric Modal Transition Systems

KŘETÍNSKÝ, Jan and Salomon SICKERT

Basic information

Original name

On Refinements of Boolean and Parametric Modal Transition Systems

Authors

KŘETÍNSKÝ, Jan (203 Czech Republic, guarantor, belonging to the institution) and Salomon SICKERT (276 Germany)

Edition

Heidelberg Dordrecht London New York, Theoretical Aspects of Computing - ICTAC 2013 - 10th International Colloquium, p. 213-230, 18 pp. 2013

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/13:00066200

Organization unit

Faculty of Informatics

ISBN

978-3-642-39717-2

ISSN

Keywords (in Czech)

modal transition systems; refinement

Keywords in English

modal transition systems; specification; interface theory; refinement

Tags

International impact, Reviewed
Změněno: 27/4/2014 23:18, RNDr. Pavel Šmerk, Ph.D.

Abstract

V originále

We consider the extensions of modal transition systems (MTS), namely Boolean MTS and parametric MTS and we investigate the refinement problems over both classes. Firstly, we reduce the problem of modal refinement over both classes to a problem solvable by a QBF solver and provide experimental results showing our technique scales well. Secondly, we extend the algorithm for thorough refinement of MTS providing better complexity than via reductions to previously studied problems. Finally, we investigate the relationship between modal and thorough refinement on the two classes and show how the thorough refinement can be approximated by the modal refinement.

Links

GAP202/10/1469, research and development project
Name: Formální metody pro analýzu a verifikaci komplexních systémů
Investor: Czech Science Foundation
MUNI/A/0760/2012, interní kód MU
Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Acronym: FI MAV II.)
Investor: Masaryk University, Category A