Regular Model Checking for LTL(MSO)

Abdulla, ParoshUppsala universitet,Institutionen för informationsteknologi,Datorteknik (author)

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.

Jonsson, BengtUppsala universitet,Institutionen för informationsteknologi,Datorteknik(Swepub:uu)bengtjs (author)
Nilsson, MarcusUppsala universitet,Institutionen för informationsteknologi,Datorteknik (author)
d'Orso, JulienUppsala universitet,Institutionen för informationsteknologi,Datorteknik (author)
Saksena, MayankUppsala universitet,Institutionen för informationsteknologi,Datorteknik(Swepub:uu)masak669 (author)
Uppsala universitetInstitutionen för informationsteknologi (creator_code:org_t)

By the author/editor: Abdulla, Parosh; Jonsson, Bengt; Nilsson, Marcus; d'Orso, Julien; Saksena, Mayank

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.