uu.seUppsala universitets publikasjoner
Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Decidability and Complexity Results for Timed Automata via Channel Machines
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
2005 Inngår i: LNCS, Vol. 3580Artikkel i tidsskrift (Fagfellevurdert) Published
sted, utgiver, år, opplag, sider
2005. Vol. 3580
Identifikatorer
URN: urn:nbn:se:uu:diva-94524OAI: oai:DiVA.org:uu-94524DiVA, id: diva2:168400
Tilgjengelig fra: 2006-05-12 Laget: 2006-05-12bibliografisk kontrollert
Inngår i avhandling
1. Verification of Parameterized and Timed Systems: Undecidability Results and Efficient Methods
Åpne denne publikasjonen i ny fane eller vindu >>Verification of Parameterized and Timed Systems: Undecidability Results and Efficient Methods
2006 (engelsk)Doktoravhandling, med artikler (Annet vitenskapelig)
Abstract [en]

Software is finding its way into an increasing range of devices (phones, medical equipment, cars...). A challenge is to design verification methods to ensure correctness of software.

We focus on model checking, an approach in which an abstract model of the implementation and a specification of requirements are provided. The task is to answer automatically whether the system conforms with its specification.We concentrate on (i) timed systems, and (ii) parameterized systems.

Timed systems can be modeled and verified using the classical model of timed automata. Correctness is translated to language inclusion between two timed automata representing the implementation and the specification. We consider variants of timed automata, and show that the problem is at best highly complex, at worst undecidable.

A parameterized system contains a variable number of components. The problem is to verify correctness regardless of the number of components. Regular model checking is a prominent method which uses finite-state automata. We present a semi-symbolic minimization algorithm combining the partition refinement algorithm by Paige and Tarjan with decision diagrams.

Finally, we consider systems which are both timed and parameterized: Timed Petri Nets (TPNs), and Timed Networks (TNs). We present a method for checking safety properties of TPNs based on forward reachability analysis with acceleration. We show that verifying safety properties of TNs is undecidable when each process has at least two clocks, and explore decidable variations of this problem.

sted, utgiver, år, opplag, sider
Uppsala: Acta Universitatis Upsaliensis, 2006. s. 29
Serie
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 187
Emneord
Parameterized Systems, Timed Systems, Symbolic Model Checking, Forward Reachability, Acceleration, Robust Languages, Language Universality, Automata Minimization, Bisimulation
Identifikatorer
urn:nbn:se:uu:diva-6891 (URN)91-554-6574-9 (ISBN)
Disputas
2006-06-02, Häggsalen, Ångström Laboratory, Polacksbacken, Lägerhyddsvägen 1, Uppsala, 10:00
Opponent
Veileder
Tilgjengelig fra: 2006-05-12 Laget: 2006-05-12 Sist oppdatert: 2011-02-18bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric

urn-nbn
Totalt: 599 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf