Sökning: onr:"swepub:oai:DiVA.org:uu-72658" >
Regular Model Check...
Regular Model Checking for LTL(MSO)
-
- Abdulla, Parosh (författare)
- Uppsala universitet,Institutionen för informationsteknologi,Datorteknik
-
- Jonsson, Bengt (författare)
- Uppsala universitet,Institutionen för informationsteknologi,Datorteknik
-
- Nilsson, Marcus (författare)
- Uppsala universitet,Institutionen för informationsteknologi,Datorteknik
-
visa fler...
-
- d'Orso, Julien (författare)
- Uppsala universitet,Institutionen för informationsteknologi,Datorteknik
-
- Saksena, Mayank (författare)
- Uppsala universitet,Institutionen för informationsteknologi,Datorteknik
-
visa färre...
-
(creator_code:org_t)
- 2004
- 2004
- Engelska.
-
Ingår i: Computer Aided Verification. - 3540223428 ; , s. 348-360
- Relaterad länk:
-
https://urn.kb.se/re...
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 words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. We present $\logic$, a combination of the logics MSO and LTL as a natural logic for expressing temporal properties to be verified in regular model checking. $\logic$ is a two-dimensional modal logic, where MSO is used for specifying properties of system states and transitions, and LTL is used for specifying temporal properties. In addition, the first-order quantification in MSO can be used to express properties parameterized on a position or process.We give a technique for model checking $\logic$, which is adapted from the automata-theoretic approach: a formula is translated to a (\buchi) transducer with a regular set of accepting states, and regular model checking techniques are used to search for models. We have implemented the technique and show its application to a number of parameterized algorithms from the literature.
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)
Hitta via bibliotek
Till lärosätets databas