@inproceedings{BhaveGuha:RP:2017,
    Abstract = {Integer reset timed automata (IRTA) are known to be a determinizable subclass of timed automata, but it is not known whether they are input-determined, i.e., the clock values are completely determined by an input timed word. We first define a syntactic subclass of IRTA called strict IRTA and show that strict IRTA is equivalent to IRTA. We show that the class of strict IRTA is indeed input-determined. Visibly pushdown automata is another input-determined class of automata with a stack that is also closed under boolean operations and admits a logical characterization. We propose dtIRVPA as a class of timed automata with a dense-timed stack. Similar to strict IRTA, we define strict dtIRVPA and show that strict dtIRVPA is input-determined where both -- stack operations and the values of the integer reset clocks -- are determined by the input word, and this helps us to get the monadic second-order (MSO) logical characterization of dtIRVPA. We prove the closure properties of dtIRVPA under union, intersection, complementation, and determinization. Further, we show that reachability of dtIRVPA is PSPACE-complete, i.e. the complexity is no more than that of timed automata.},
    Address = {Cham},
    Author = {Bhave, Devendra and Guha, Shibashis},
    BookTitle = {Proc. of RP'17},
    Editor = {Hague, Matthew and Potapov, Igor},
    File = {Adding Dense-Timed Stack to Integer Reset Timed Automata - Bhave-Guha2017\_Chapter\_AddingDense-TimedStackToIntege - a - a - z.pdf},
    ISBN = {978-3-319-67089-8},
    Keywords = {timed automata and pushdown automata and citesme!},
    Pages = {9--25},
    Publisher = {Springer},
    Title = {Adding Dense-Timed Stack to Integer Reset Timed Automata},
    URL = {https://doi.org/10.1007/978-3-319-67089-8\_2},
    Year = {2017},
    bdsk-url-1 = {https://doi.org/10.1007/978-3-319-67089-8\_2},
    bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-319-67089-8\_2},
    date-added = {2017-09-05 08:59:03 +0000},
    date-modified = {2019-08-16 16:53:38 +0200},
    doi = {10.1007/978-3-319-67089-8_2}
}

@inproceedings{BhaveGuha:RP:2017, Abstract = {Integer reset timed automata (IRTA) are known to be a determinizable subclass of timed automata, but it is not known whether they are input-determined, i.e., the clock values are completely determined by an input timed word. We first define a syntactic subclass of IRTA called strict IRTA and show that strict IRTA is equivalent to IRTA. We show that the class of strict IRTA is indeed input-determined. Visibly pushdown automata is another input-determined class of automata with a stack that is also closed under boolean operations and admits a logical characterization. We propose dtIRVPA as a class of timed automata with a dense-timed stack. Similar to strict IRTA, we define strict dtIRVPA and show that strict dtIRVPA is input-determined where both -- stack operations and the values of the integer reset clocks -- are determined by the input word, and this helps us to get the monadic second-order (MSO) logical characterization of dtIRVPA. We prove the closure properties of dtIRVPA under union, intersection, complementation, and determinization. Further, we show that reachability of dtIRVPA is PSPACE-complete, i.e. the complexity is no more than that of timed automata.}, Address = {Cham}, Author = {Bhave, Devendra and Guha, Shibashis}, BookTitle = {Proc. of RP'17}, Editor = {Hague, Matthew and Potapov, Igor}, File = {Adding Dense-Timed Stack to Integer Reset Timed Automata - Bhave-Guha2017_Chapter_AddingDense-TimedStackToIntege - a - a - z.pdf}, ISBN = {978-3-319-67089-8}, Keywords = {timed automata and pushdown automata and citesme!}, Pages = {9--25}, Publisher = {Springer}, Title = {Adding Dense-Timed Stack to Integer Reset Timed Automata}, URL = {https://doi.org/10.1007/978-3-319-67089-8_2}, Year = {2017}, bdsk-url-1 = {https://doi.org/10.1007/978-3-319-67089-8_2}, bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-319-67089-8_2}, date-added = {2017-09-05 08:59:03 +0000}, date-modified = {2019-08-16 16:53:38 +0200}, doi = {10.1007/978-3-319-67089-8_2} }