Change search
ReferencesLink to record
Permanent link

Direct link
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
IT, 12 034
National Category
Engineering and Technology
URN: urn:nbn:se:uu:diva-179802OAI: diva2:546296
Educational program
Bachelor Programme in Computer Science
Available from: 2012-08-23 Created: 2012-08-23 Last updated: 2012-08-23Bibliographically approved

Open Access in DiVA

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

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 355 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

Total: 444 hits
ReferencesLink to record
Permanent link

Direct link