@book(LAKJ1,
 author       = "L. Aceto and A. Ing$\mathaccentV {acute}013{o}$lfsd$\mathaccentV {acute}013{o}$ttir and K.G. Larsen and J. Srba",
 year         = "2007",
 title        = "Reactive Systems: Modelling, Specification and Verification",
 publisher    = "Cambridge University Press",
 doi          = "10.1145/1811226.1811243",
)
@inproceedings(ACH1,
 author       = "R. Alur and C. Courcoubetis and T. A. Henzinger",
 year         = "1994",
 title        = "The Observational Power of Clocks",
 booktitle    = "Proceedings of CONCUR",
 pages        = "162--177",
 doi          = "10.1007/BFb0015008",
)
@article(AD1,
 author       = "R. Alur and D.L. Dill",
 year         = "1994",
 title        = "A Theory of Timed Automata",
 journal      = "Theoretical Computer Science",
 volume       = "126",
 pages        = "183--235",
 doi          = "10.1016/0304-3975(94)90010-8",
)
@inproceedings(KC1,
 author       = "K. Cerans",
 year         = "1992",
 title        = "Decidability of bisimulation equivalences for parallel timer processes",
 booktitle    = "Proceedings of CAV",
 volume       = "663",
 publisher    = "Springer-Verlag",
 pages        = "302--315",
 doi          = "10.1007/3-540-56496-9\_24",
)
@inproceedings(CD1,
 author       = "X. Chen and Y. Deng",
 year         = "2008",
 title        = "Game Characterizations of Process Equivalences",
 booktitle    = "Proceedings of APLAS",
 pages        = "107--121",
 doi          = "10.1007/978-3-540-89330-1\_8",
)
@inproceedings(DT1,
 author       = "C. Daws and S. Tripakis",
 year         = "1998",
 title        = "Model Checking of Real-Time Reachability Properties Using Abstractions",
 booktitle    = "Proceedings of TACAS",
 publisher    = "Springer-Verlag",
 pages        = "313--329",
 doi          = "10.1007/BFb0054180",
)
@inproceedings(BBFL1,
 author       = "E. Fleury G. Behrmann, P. Bouyer and K. G. Larsen",
 year         = "2003",
 title        = "Static guard analysis in timed automata verification",
 booktitle    = "Proceedings of TACAS",
 publisher    = "Springer-Verlag",
 pages        = "254--270",
 doi          = "10.1007/3-540-36577-X\_18",
)
@article(BBLP1,
 author       = "K. G. Larsen G. Behrmann, P. Bouyer and R. Pelanek",
 year         = "2006",
 title        = "Lower and upper bounds in zone-based abstractions of timed automata",
 journal      = "International Journal on Software Tools for Technology Transfer",
 volume       = "8",
 pages        = "204--215",
 doi          = "10.1007/s10009-005-0190-0",
)
@inproceedings(VG1,
 author       = "Rob J. van Glabbeek",
 year         = "1990",
 title        = "The Linear Time-Branching Time Spectrum (Extended Abstract)",
 booktitle    = "Proceedings of CONCUR",
 pages        = "278--297",
 doi          = "10.1007/BFb0039066",
)
@article(GL1,
 author       = "J. C. Godskesen and K. G. Larsen",
 year         = "1995",
 title        = "Synthesizing distinguishing formulae for real time systems",
 journal      = "Nordic J. of Computing",
 volume       = "2",
 number       = "3",
 pages        = "338--357",
)
@inproceedings(GNA1,
 author       = "S. Guha and C. Narayan and S. Arun-Kumar",
 year         = "2012",
 title        = "On Decidability of Prebisimulation for Timed Automata",
 booktitle    = "Proceedings of CAV",
 publisher    = "Springer-Verlag",
 pages        = "444--461",
 doi          = "10.1007/978-3-642-31424-7\_33",
)
@article(HNSY1,
 author       = "T. A. Henzinger and X. Nicollin and J. Sifakis and S. Yovine",
 year         = "1992",
 title        = "Symbolic Model Checking for Real-time Systems",
 journal      = "Information and Computation",
 volume       = "111",
 pages        = "394--406",
 doi          = "10.1006/inco.1994.1045",
)
@article(KNSS1,
 author       = "M. Kwiatkowska and G. Norman and R. Segala and J. Sproston",
 year         = "2002",
 title        = "Automatic verification of real-time systems with discrete probability distributions",
 journal      = "Theoretical Computer Science",
 volume       = "282",
 number       = "1",
 pages        = "101--150",
 doi          = "10.1016/S0304-3975(01)00046-9",
)
@inproceedings(LLW1,
 author       = "F. Laroussinie and Kim G. Larsen and C. Weise",
 year         = "1995",
 title        = "From Timed Automata to Logic -- and Back",
 booktitle    = "Proceedings of MFCS",
 pages        = "529--539",
 doi          = "10.1007/3-540-60246-1\_158",
)
@inproceedings(LH1,
 author       = "F. Laroussinie and Ph. Schnoebelen",
 year         = "2000",
 title        = "The State Explosion Problem from Trace to Bisimulation Equivalence",
 booktitle    = "Proceedings of FoSSaCS",
 publisher    = "Springer-Verlag",
 pages        = "192--207",
 doi          = "10.1007/3-540-46432-8\_13",
)
@inproceedings(LY1,
 author       = "K. G. Larsen and W. Yi",
 year         = "1994",
 title        = "Time abstracted bisimulation: implicit specifications and decidability",
 booktitle    = "Proceedings of MFPS",
 volume       = "802",
 publisher    = "Springer-Verlag",
 pages        = "160--176",
 doi          = "10.1007/3-540-58027-1\_8",
)
@book(RM1,
 author       = "R. Milner",
 year         = "1989",
 title        = "Communication and Concurrency",
 publisher    = "Prentice Hall",
)
@inproceedings(CS1,
 author       = "C. Stirling",
 year         = "1995",
 title        = "Local Model Checking Games",
 booktitle    = "Proceedings of CONCUR",
 pages        = "1--11",
 doi          = "10.1007/3-540-60218-6\_1",
)
@book(CS2,
 author       = "C. Stirling",
 year         = "2001",
 title        = "Modal and temporal properties of processes",
 publisher    = "Springer-Verlag New York, Inc.",
 address      = "New York, NY, USA",
 doi          = "10.1007/978-1-4757-3550-5",
)
@book(HS1,
 author       = "H. Straubing",
 year         = "1994",
 title        = "Finite automata, formal logic, and circuit complexity",
 publisher    = "Birkhauser Verlag",
 address      = "Basel, Switzerland, Switzerland",
 doi          = "10.1007/978-1-4612-0289-9",
)
@article(TY1,
 author       = "S. Tripakis and S. Yovine",
 year         = "2001",
 title        = "Analysis of Timed Systems using Time-Abstracting Bisimulations",
 journal      = "Formal Methods in System Design",
 volume       = "18",
 pages        = "25--68",
 doi          = "10.1023/A:1008734703554",
)
@inproceedings(WL1,
 author       = "C. Weise and D. Lenzkes",
 year         = "1997",
 title        = "Efficient scaling-invariant checking of timed bisimulation",
 booktitle    = "Proceedings of STACS",
 volume       = "1200",
 publisher    = "Springer, Berlin",
 pages        = "177--188",
 doi          = "10.1007/BFb0023458",
)