Linear reachability problems and minimal solutions to linear Diophantine equation systems

The linear reachability problem for finite state transition systems is to decide whether there is an execution path in a given finite state transition system such that the counts of labels on the path satisfy a given linear constraint. Using some known results on minimal solutions (in nonnegative in...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2004-11, Vol.328 (1), p.203-219
Main Authors: Xie, Gaoyan, Li, Cheng, Dang, Zhe
Format: Article
Language:English
Subjects:
Algebra
Applied sciences
Automata. Abstract machines. Turing machines
Computer science
control theory
systems
Exact sciences and technology
Linear Diophantine equation systems
Mathematics
Minimal solutions
Model-checking
Number theory
Reachability
Sciences and techniques of general use
Theoretical computing
Timed automata
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The linear reachability problem for finite state transition systems is to decide whether there is an execution path in a given finite state transition system such that the counts of labels on the path satisfy a given linear constraint. Using some known results on minimal solutions (in nonnegative integers) for linear Diophantine equation systems, we present new time complexity bounds for the problem. In contrast to the previously known results, the bounds obtained in this paper are polynomial in the size of the transition system in consideration, when the linear constraint is fixed. The bounds are also used to establish a worst-case time complexity result for the linear reachability problem for timed automata.
ISSN:0304-3975
1879-2294
DOI:10.1016/j.tcs.2004.07.015