BENEŠ, Nikola, Ivana ČERNÁ and Jan KŘETÍNSKÝ. Modal Transition Systems: Composition and LTL Model Checking. In ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium. Heidelberg Dordrecht London New York: Springer, 2011. p. 228-242. ISBN 978-3-642-24371-4.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Modal Transition Systems: Composition and LTL Model Checking
Authors BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Ivana ČERNÁ (203 Czech Republic, belonging to the institution) and Jan KŘETÍNSKÝ (203 Czech Republic, guarantor, belonging to the institution).
Edition Heidelberg Dordrecht London New York, ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium, p. 228-242, 15 pp. 2011.
Publisher Springer
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
RIV identification code RIV/00216224:14330/11:00049982
Organization unit Faculty of Informatics
ISBN 978-3-642-24371-4
UT WoS 000306498800017
Keywords in English modal transition systems; model checking; refinement; conjunction
Tags International impact, Reviewed
Changed by Changed by: RNDr. Nikola Beneš, Ph.D., učo 72525. Changed: 24. 10. 2013 16:21.
Abstract
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.
Links
GAP202/11/0312, research and development projectName: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Acronym: Components in Embedded Systems)
Investor: Czech Science Foundation
GD102/09/H042, research and development projectName: Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
Investor: Czech Science Foundation
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
MUNI/A/0914/2009, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV)
Investor: Masaryk University, Category A
Type Name Uploaded/Created by Uploaded/Created Rights
paper_51-1_hqkmdxut.pdf  Černá, I. 2. 12. 2011

Properties

Address within IS
https://is.muni.cz/auth/publication/950140/paper_51-1_hqkmdxut.pdf
Address for the users outside IS
https://is.muni.cz/publication/950140/paper_51-1_hqkmdxut.pdf
Address within Manager
https://is.muni.cz/auth/publication/950140/paper_51-1_hqkmdxut.pdf?info
Address within Manager for the users outside IS
https://is.muni.cz/publication/950140/paper_51-1_hqkmdxut.pdf?info
Uploaded/Created
Fri 2. 12. 2011 09:23, prof. RNDr. Ivana Černá, CSc.

Rights

Right to read
  • anyone on the Internet
Right to upload
 
Right to administer:
  • a concrete person doc. Dr. rer. nat. RNDr. Mgr. Bc. Jan Křetínský, Ph.D., učo 139914
  • a concrete person prof. RNDr. Ivana Černá, CSc., učo 1419
  • a concrete person RNDr. Nikola Beneš, Ph.D., učo 72525
Attributes
 

paper_51-1_hqkmdxut.pdf

Application
Open the file
Download file.
Address within IS
https://is.muni.cz/auth/publication/950140/paper_51-1_hqkmdxut.pdf
Address for the users outside IS
http://is.muni.cz/publication/950140/paper_51-1_hqkmdxut.pdf
File type
PDF (application/pdf)
Size
357,1 KB
Hash md5
5aa177a40ffc12ab5438dcaf5a96024b
Uploaded/Created
Fri 2. 12. 2011 09:23

paper_51-1_hqkmdxut.txt

Application
Open the file
Download file.
Address within IS
https://is.muni.cz/auth/publication/950140/paper_51-1_hqkmdxut.txt
Address for the users outside IS
http://is.muni.cz/publication/950140/paper_51-1_hqkmdxut.txt
File type
plain text (text/plain)
Size
40,3 KB
Hash md5
be9eb36c0cae331ec330d4e9644f5e4c
Uploaded/Created
Fri 2. 12. 2011 09:26
Print
Report a file uploaded without authorization. Displayed: 20. 5. 2022 23:04