BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC and Jiří ŠIMŠA. Under-Approximation Generation using Partial Order Reduction. Brno: Faculty of Informatics, 2005, 21 pp. Technical Reports, FIMU-RS-2005-04.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Under-Approximation Generation using Partial Order Reduction
Name in Czech Generování stavového prostoru s použitím under-aproximace a partial order reduction
Authors BRIM, Luboš (203 Czech Republic, guarantor), Ivana ČERNÁ (203 Czech Republic), Pavel MORAVEC (203 Czech Republic) and Jiří ŠIMŠA (203 Czech Republic).
Edition Brno, 21 pp. Technical Reports, FIMU-RS-2005-04, 2005.
Publisher Faculty of Informatics
Other information
Original language English
Type of outcome Book on a specialized topic
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
WWW URL
RIV identification code RIV/00216224:14330/05:00012458
Organization unit Faculty of Informatics
Keywords in English under-aproximation; state space generation; partial order reduction
Tags partial order reduction, state space generation, under-aproximation
Tags International impact
Changed by Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 19/12/2006 13:19.
Abstract
We propose a new on-the-fly approach which combines partial order reduction with the under-approximation technique for falsification and verification of LTL-X properties. It uses sensitivity relation and modified ample conditions to generate a reduced state space that is not fully stutter equivalent to the original one and it checks the desired property using representatives. Widening of under-approximations is fully automatic and does not rely on any supporting mechanisms like theorem-provers or SAT solvers.
Abstract (in Czech)
V práci je navržen nový způsob generování stavových prostorů kombinující metody partial order reduction s under-approximacemi pro ověřování LTL-X vlastností modelu. Používá relaci sensitivity a modifikované podmínky na ample-sets. Výsledný redukovaný stavový prostor není plně ekvivalentní původnímu, v práci jsou proto navrženy rozšíření under-aproximací, které lze provádět automaticky a nepotřebují další pomocné mechanismy jako jsou theorem-proovers nebo SAT solvery.
Links
GA201/03/0509, research and development projectName: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Czech Science Foundation, Automated Verification of Parallel and Distributed Systems
PrintDisplayed: 9/8/2024 00:02