Sökning: onr:"swepub:oai:DiVA.org:uu-529294" >
Algorithmic Improve...
Algorithmic Improvements in Regular Model Checking
-
- Abdulla, Parosh Aziz (författare)
- Uppsala universitet,Institutionen för informationsteknologi
-
Jonsson, Bengt (författare)
-
Nilsson, Marcus (författare)
-
visa fler...
-
d'Orso, Julien (författare)
-
visa färre...
-
(creator_code:org_t)
- Department of Information Technology, Uppsala University, 2003
- Engelska.
-
Serie: Technical report / Department of Information Technology, Uppsala University, 1404-3203 ; 2003-024
- Relaterad länk:
-
https://uu.diva-port... (primary) (Raw object)
-
visa fler...
-
https://urn.kb.se/re...
-
visa färre...
Abstract
Ämnesord
Stäng
- Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems, whose states can be represented as finite strings of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. In earlier papers, we have developed methods for computing the transitive closure (or the set of reachable states) of the transition relation, represented by a regular length-preserving transducer. In this paper, we present several improvements of these techniques, which reduce the size of intermediate approximations of the transitive closure: One improvement is to pre-process the transducer by \em bi-determinization, another is to use a more powerful equivalence relation for identifying histories (columns) of states in the transitive closure. We also present a simplified theoretical framework for showing soundness of the optimization, which is based on commuting simulations. The techniques have been implemented, and we report the speedups obtained from the respective optimizations.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Publikations- och innehållstyp
- vet (ämneskategori)
- rap (ämneskategori)