Relaxed Cycle Condition Improves Partial Order Reduction
MORAVEC, Pavel and Jiří ŠIMŠA. Relaxed Cycle Condition Improves Partial Order Reduction. In 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007). Znojmo, Czech Republic: FI MU, FIT VUT, 2007, p. 140-147. ISBN 978-80-7355-077-6. |
Other formats:
BibTeX
LaTeX
RIS
|
Basic information | |
---|---|
Original name | Relaxed Cycle Condition Improves Partial Order Reduction |
Name in Czech | Oslabení podmínky na cykly zlepšující redukci pomocí reprezentantů |
Authors | MORAVEC, Pavel (203 Czech Republic, guarantor) and Jiří ŠIMŠA (203 Czech Republic). |
Edition | Znojmo, Czech Republic, 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007), p. 140-147, 2007. |
Publisher | FI MU, FIT VUT |
Other information | |
---|---|
Original language | English |
Type of outcome | Proceedings paper |
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 |
RIV identification code | RIV/00216224:14330/07:00019497 |
Organization unit | Faculty of Informatics |
ISBN | 978-80-7355-077-6 |
Keywords in English | model checking; partial order reduction; proviso checking |
Tags | Model checking, partial order reduction, proviso checking |
Changed by | Changed by: Mgr. Pavel Moravec, učo 39589. Changed: 28/11/2007 10:10. |
Abstract |
---|
Partial order reduction is a method widely used for tackling the state space explosion problem. In this paper we focus on a theoretical refinement of a particular instance of the partial order reduction which is nowadays an inherent part of most tools for explicit state model checking of Linear Temporal Logic. This particular instance is represented as a set of conditions C0 through C3 which describe valid reductions of a state space. We propose a hierarchy of alternatives to the cycle condition C3. In this hierarchy we point out which alternatives guarantee a valid reduction with respect to LTL_X properties. |
Abstract (in Czech) |
---|
Redukce pomocí reprezentantů je metoda široce používaná na boj se stavovou explozí. V článku se zaměřujeme na teoretické zjemnění konkrétní instance této redukce pro logiku LTL. Tato instance je representována množinou podmínek C0 až C3 které popisují platné redukce stavového prostoru. Navrhujeme hierarchii alternativ k podmínce C3. V této hierarchii ukážeme které alternativy k C3 garantují platnou redukci vzhledem k LTL vlastnostem. |
Links | |
---|---|
GA201/06/1338, research and development project | Name: Automatizovaná verifikace softwaru |
Investor: Czech Science Foundation, Automated software verification | |
GD102/05/H050, research and development project | Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů |
Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed 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 | |
1ET408050503, research and development project | Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů |
Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems | |
1M0545, research and development project | Name: Institut Teoretické Informatiky |
Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science |
PrintDisplayed: 9/10/2024 23:04