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
Tree Regular Model Checking: A simulation-based approach
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.
2006 (English)In: Journal of Logic and Algebraic Programming, ISSN 1567-8326, E-ISSN 1873-5940, Vol. 69, no 1-2, 93-121 p.Article in journal (Refereed) Published
Abstract [en]

Regular model checking is the name of a family of techniques for analyzing infinite-state systems in which states are represented by words, sets of states by finite automata, and transitions by finite-state transducers. In this framework, the central problem is to compute the transitive closure of a transducer. Such a representation allows to compute the set of reachable states of the system and to detect loops between states. A main obstacle of this approach is that there exists many systems for which the reachable set of states is not regular. Recently, regular model checking has been extended to systems with tree-like architectures. In this paper, we provide a procedure, based on a new implementable acceleration technique, for computing the transitive closure of a tree transducer. The procedure consists of incrementally adding new transitions while merging states, which are related according to a pre-defined equivalence relation. The equivalence is induced by a downward and an upward simulation relation, which can be efficiently computed. Our technique can also be used to compute the set of reachable states without computing the transitive closure. We have implemented and applied our technique to various protocols.

Place, publisher, year, edition, pages
2006. Vol. 69, no 1-2, 93-121 p.
Keyword [en]
tree regular model checking, transducer, semi-algorithm, simulation, rewrite systems
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:uu:diva-20250DOI: 10.1016/j.jlap.2006.02.001ISI: 000240303000003OAI: oai:DiVA.org:uu-20250DiVA: diva2:48023
Available from: 2006-12-07 Created: 2006-12-07 Last updated: 2017-12-08Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text
By organisation
Computer Systems
In the same journal
Journal of Logic and Algebraic Programming
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 394 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