Record Details

Model checking logic WCTL with multi constrained modalities on one clock priced timed automata

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title Model checking logic WCTL with multi constrained modalities on one clock priced timed automata
 
Creator CHIPLUNKAR, A
KRISHNA, SN
JAIN, C
 
Subject optimal reachability
 
Description We consider the model of priced timed automata, an extension of timed automata and study the model checking problem of logic WCTL with multi constrained modalities. For simple modalities, it is known that this is decidable [10] for one clock priced timed automata, and is not [14] when the number of clocks is more than one. For the model of priced timed automata with 2 stopwatch costs having no discrete costs, we give an algorithm for model checking the existential fragment of WCTL with multi constrained modalities. The algorithm runs in time that is doubly exponential in the size of the input(automaton, formula).
 
Publisher SPRINGER-VERLAG BERLIN
 
Date 2011-10-24T02:01:17Z
2011-12-15T09:11:22Z
2011-10-24T02:01:17Z
2011-12-15T09:11:22Z
2009
 
Type Proceedings Paper
 
Identifier FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, PROCEEDINGS,5813,88-102
978-3-642-04367-3
0302-9743
http://dspace.library.iitb.ac.in/xmlui/handle/10054/15301
http://hdl.handle.net/100/2024
 
Source 7th International Conference on Formal Modeling and Analysis of Timed Systems,Budapest, HUNGARY,SEP 14-16, 2009
 
Language English