Thesis
Complexity analysis of the Presburger reachability problem for discrete timed automata
Washington State University
Master of Science (MS), Washington State University
2002
Handle:
https://hdl.handle.net/2376/86
Abstract
The Presburger reachability for discrete timed automata is to decide whether some clock values in a Presburger clock constraint are reachable in a discrete timed automaton. We present a procedure to solve this problem. The procedure constructs a finite state machine from an instance of the problem. The construction involves calculations of the minimal solutions to some linear Diophantine equations. An upper bound for the time complexity of the procedure is obtained in the thesis. This result helps to build an automatic verification tool for real-time systems in the future. However, from some preliminary experiments, we conclude that some optimization techniques shall be further developed in order for the procedure to be working on a large instance.
Metrics
1 File views/ downloads
9 Record Views
Details
- Title
- Complexity analysis of the Presburger reachability problem for discrete timed automata
- Creators
- Cheng Li
- Contributors
- Zhe Dang (Degree Supervisor)
- Awarding Institution
- Washington State University
- Academic Unit
- Electrical Engineering and Computer Science, School of
- Theses and Dissertations
- Master of Science (MS), Washington State University
- Publisher
- Washington State University; Pullman, Wash. :
- Identifiers
- 99900525401001842
- Language
- English
- Resource Type
- Thesis