SwePub
Sök i LIBRIS databas

  Extended search

id:"swepub:oai:DiVA.org:uu-48996"
 

Search: id:"swepub:oai:DiVA.org:uu-48996" > Forward Reachabilit...

  • 1 of 1
  • Previous record
  • Next record
  •    To hitlist
  • Abdulla, Parosh AzizUppsala universitet,Datorteknik,COMPUTER SYSTEMS (author)

Forward Reachability Analysis of Timed Petri Nets

  • BookEnglish2003

Publisher, publication year, extent ...

  • Uppsala: Department of Information Technology, Uppsala University,2003
  • electronicrdacarrier

Numbers

  • LIBRIS-ID:oai:DiVA.org:uu-48996
  • https://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-48996URI

Supplementary language notes

  • Language:English
  • Summary in:English

Part of subdatabase

Classification

  • Subject category:vet swepub-contenttype
  • Subject category:rap swepub-publicationtype

Series

  • Technical report / Department of Information Technology, Uppsala University,1404-3203 ;2003-056

Notes

  • We consider verification of safety properties for concurrent real-timed systems modelled by timed Petri nets, by performing symbolic forward reachability analysis. We introduce a formalism, called region generators for representing sets of markings of timed Petri nets. Region generators characterize downward closed sets of regions. Downward closed languages provide exact abstractions of sets of reachable states with respect to safety properties.We show that the standard operations needed for performing symbolic reachability analysis are computable for region generators. Since forward reachability analysis is necessarily incomplete, we introduce an acceleration technique to make the procedure terminate more often on practical examples.We have implemented a prototype for analyzing timed Petri nets and used it to verify a parameterized version of Fischer's protocol. We also used the tool to generate a finite-state abstraction of the protocol.

Subject headings and genre

Added entries (persons, corporate bodies, meetings, titles ...)

  • Deneux, Johann (author)
  • Mahata, Pritha (author)
  • Nylén, Aletta (author)
  • Uppsala universitetDatorteknik (creator_code:org_t)

Internet link

To the university's database

  • 1 of 1
  • Previous record
  • Next record
  •    To hitlist

Find more in SwePub

By the author/editor
Abdulla, Parosh ...
Deneux, Johann
Mahata, Pritha
Nylén, Aletta
About the subject
NATURAL SCIENCES
NATURAL SCIENCES
and Computer and Inf ...
Parts in the series
Technical report ...
By the university
Uppsala University

Search outside SwePub

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.

 
pil uppåt Close

Copy and save the link in order to return to this view