uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Regular model checking for LTL(MSO)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Show others and affiliations
2012 (English)In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1385-4879, E-ISSN 1571-8115, Vol. 14, no 2, 223-241 p.Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer, 2012. Vol. 14, no 2, 223-241 p.
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-189970DOI: 10.1007/s10009-011-0212-zOAI: oai:DiVA.org:uu-189970DiVA: diva2:582622
Projects
UPMARC
Available from: 2013-01-05 Created: 2013-01-05 Last updated: 2017-12-06Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Jonsson, Bengt

Search in DiVA

By author/editor
Jonsson, Bengt
By organisation
Computer Systems
In the same journal
International Journal on Software Tools for Technology Transfer (STTT)
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 453 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf