Sökning: WFRF:(d'Orso Julien) >
Regular Model Check...
-
Abdulla, ParoshUppsala universitet,Institutionen för informationsteknologi,Datorteknik
(författare)
Regular Model Checking for LTL(MSO)
- Artikel/kapitelEngelska2004
Förlag, utgivningsår, omfång ...
Nummerbeteckningar
-
LIBRIS-ID:oai:DiVA.org:uu-72658
-
https://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-72658URI
Kompletterande språkuppgifter
-
Språk:engelska
-
Sammanfattning på:engelska
Ingår i deldatabas
Klassifikation
-
Ämneskategori:ref swepub-contenttype
-
Ämneskategori:kon swepub-publicationtype
Anmärkningar
-
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.
Biuppslag (personer, institutioner, konferenser, titlar ...)
-
Jonsson, BengtUppsala universitet,Institutionen för informationsteknologi,Datorteknik(Swepub:uu)bengtjs
(författare)
-
Nilsson, MarcusUppsala universitet,Institutionen för informationsteknologi,Datorteknik
(författare)
-
d'Orso, JulienUppsala universitet,Institutionen för informationsteknologi,Datorteknik
(författare)
-
Saksena, MayankUppsala universitet,Institutionen för informationsteknologi,Datorteknik(Swepub:uu)masak669
(författare)
-
Uppsala universitetInstitutionen för informationsteknologi
(creator_code:org_t)
Sammanhörande titlar
-
Ingår i:Computer Aided Verification, s. 348-3603540223428
Internetlänk
Hitta via bibliotek
Till lärosätets databas