Sökning: L773:1433 2779 OR L773:1433 2787 >
Regular model check...
Regular model checking for LTL(MSO)
-
- Abdulla, Parosh (författare)
- Uppsala universitet,Datorteknik
-
- Jonsson, Bengt (författare)
- Uppsala universitet,Datorteknik
-
- Nilsson, Marcus (författare)
- Uppsala universitet,Datorteknik
-
visa fler...
-
- d'Orso, Julien (författare)
- Uppsala universitet,Datorteknik
-
- Saksena, Mayank (författare)
- Uppsala universitet,Datorteknik
-
visa färre...
-
(creator_code:org_t)
- 2011-08-25
- 2012
- Engelska.
-
Ingår i: International Journal on Software Tools for Technology Transfer. - Springer : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 14:2, s. 223-241
- Relaterad länk:
-
https://urn.kb.se/re...
-
visa fler...
-
https://doi.org/10.1...
-
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 words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. We present LTL(MSO), a combination of the logics MSO and LTL as a natural logic for expressing temporal properties to be verified in regular model checking. In other words, LTL(MSO) is a natural specification language for both the system and the property under consideration. LTL(MSO) 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 LTL(MSO), which is adapted from the automata-theoretic approach: a formula is translated to a Buechi regular transition system 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Publikations- och innehållstyp
- ref (ämneskategori)
- art (ämneskategori)
Hitta via bibliotek
Till lärosätets databas