BENEŠ, Nikola, Luboš BRIM, Barbora BÜHNOVÁ, Ivana ČERNÁ, Jiří SOCHOR and Pavlína MORAVCOVÁ VAŘEKOVÁ. Partial Order Reduction for State/Event LTL with Application to Component-Interaction Automata. Science of Computer Programming. Elsevier, 2011, vol. 76, No 10, p. 877-890. ISSN 0167-6423. doi:10.1016/j.scico.2010.02.008.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Partial Order Reduction for State/Event LTL with Application to Component-Interaction Automata
Authors BENEŠ, Nikola (203 Czech Republic, guarantor, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution), Barbora BÜHNOVÁ (203 Czech Republic, belonging to the institution), Ivana ČERNÁ (203 Czech Republic, belonging to the institution), Jiří SOCHOR (203 Czech Republic, belonging to the institution) and Pavlína MORAVCOVÁ VAŘEKOVÁ (203 Czech Republic, belonging to the institution).
Edition Science of Computer Programming, Elsevier, 2011, 0167-6423.
Other information
Original language English
Type of outcome Article in a journal
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Czech Republic
Confidentiality degree is not subject to a state or trade secret
Impact factor Impact factor: 0.622
RIV identification code RIV/00216224:14330/11:00049649
Organization unit Faculty of Informatics
UT WoS 000292232900004
Keywords in English State/event LTL; Partial order reduction; Formal verification; Model checking; Component-based systems; Component-interaction automata
Tags International impact, Reviewed
Changed by Changed by: RNDr. Nikola Beneš, Ph.D., učo 72525. Changed: 24. 10. 2013 16:21.
Software systems assembled from autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL (Chaki et al. 2004, 2005) incorporates both states and events to express important properties of component-based software systems. The main contribution of this paper is a partial order reduction technique for verification of state/event LTL properties. The core is a novel notion of stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence. To bring some evidence of the method’s efficiency, we present the results obtained by employing the partial order reduction technique within our tool for verification of component-based systems.
GA201/09/1389, research and development projectName: Verifikace a analýza velmi velkých počítačových systémů
Investor: Czech Science Foundation, Verification and Analysis of Large-Scale Computer Systems
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
PrintDisplayed: 3. 7. 2022 17:01