Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Tree Regular Model Checking: A simulation-based approach
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
2006 (Engelska)Ingår i: Journal of Logic and Algebraic Programming, ISSN 1567-8326, E-ISSN 1873-5940, Vol. 69, nr 1-2, 93-121 s.Artikel i tidskrift (Refereegranskat) 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.

Ort, förlag, år, upplaga, sidor
2006. Vol. 69, nr 1-2, 93-121 s.
Nyckelord [en]
tree regular model checking, transducer, semi-algorithm, simulation, rewrite systems
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
URN: urn:nbn:se:uu:diva-20250DOI: 10.1016/j.jlap.2006.02.001ISI: 000240303000003OAI: oai:DiVA.org:uu-20250DiVA: diva2:48023
Tillgänglig från: 2006-12-07 Skapad: 2006-12-07 Senast uppdaterad: 2011-06-20Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas

Övriga länkar

Förlagets fulltext
Av organisationen
Datorteknik
I samma tidskrift
Journal of Logic and Algebraic Programming
Data- och informationsvetenskap

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 380 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf