Real-Time Model-Checking: Parameters everywhere

Details Real-Time Model-Checking: Parameters everywhere Real-Time Model-Checking: Parameters everywhere

2007-01-22

arxiv.org/abs/cs/0701138v2

LMCS 3 (1:7) 2007

Computer Science

Logic in Computer Science

Scientific paper

10.2168/LMCS-3(1:7)2007

In this paper, we study the model-checking and parameter synthesis problems of the logic TCTL over discrete-timed automata where parameters are allowed both in the model (timed automaton) and in the property (temporal formula). Our results are as follows. On the negative side, we show that the model-checking problem of TCTL extended with parameters is undecidable over discrete-timed automata with only one parametric clock. The undecidability result needs equality in the logic. On the positive side, we show that the model-checking and the parameter synthesis problems become decidable for a fragment of the logic where equality is not allowed. Our method is based on automata theoretic principles and an extension of our method to express durations of runs in timed automata using Presburger arithmetic.

Affiliated with

Also associated with

No associations

Rating

Real-Time Model-Checking: Parameters everywhere does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Real-Time Model-Checking: Parameters everywhere, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Real-Time Model-Checking: Parameters everywhere will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-516110