Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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
Zone-Based Reachability Analysis of Dense-Timed Pushdown Automata
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
2012 (English)Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesis
Abstract [en]

Proving that programs behave correctly is a matter of both great theoretical interest as well as practical use. One way to do this is by analyzing a model of the system in question in order to determine if it meets a given specification. Real-time recursive systems can be modeled by dense-timed pushdown automata, a model which combines the behaviours of classical timed automata and pushdown automata. The problem of reachability has been proven to be decidable for this model. The algorithm that solves this problem relies on constructing a classical pushdown automaton that mimics the behaviour of a given timed pushdown automaton by means of an abstraction that uses regions as a symbolic representation  of states. The drawback of this approach is that the untimed automaton produced generally contains a very large number of states. This report  proposes a method of generalizing this abstraction by using zones instead of regions, in order to minimize the number of states in the untimed automaton.

Place, publisher, year, edition, pages
2012.
Series
IT, 12 034
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:uu:diva-179802OAI: oai:DiVA.org:uu-179802DiVA: diva2:546296
Educational program
Bachelor Programme in Computer Science
Uppsok
Technology
Supervisors
Examiners
Available from: 2012-08-23 Created: 2012-08-23 Last updated: 2012-08-23Bibliographically approved

Open Access in DiVA

fulltext(749 kB)387 downloads
File information
File name FULLTEXT01.pdfFile size 749 kBChecksum SHA-512
ec4dc5024e91e852007f2c612633ed143f1885aa34750075f14addaa70f3d8c9299c7076c786d16568c5a1c8c64ce8e1b35c975cd998ed0e95fda9fd0ae03788
Type fulltextMimetype application/pdf

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 387 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 673 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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