@inproceedings{4621,
  abstract     = {The  most  natural,  compositional,  way  of  modeling  real-time  systems  uses  a  dense domain  for  time.  The  satisfiability  of  timing  constraints  that  are  capable  of  expressing  punctuality in  this  model,  however,  is  known  to  be  undecidable.  We  introduce  a  temporal  language  that  can constrain  the  time  difference  between  events  only  with  finite,  yet  arbitrary,  precision  and  show  the resulting  logic  to  be  EXPSPACE-complete.  This  result  allows  us  to  develop  an  algorithm  for  the verification  of  timing  properties  of  real-time  systems  with  a  dense  semantics.},
  author       = {Alur, Rajeev and Feder, Tomás and Henzinger, Thomas A},
  booktitle    = {Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing},
  isbn         = {978-0-89791-439-0},
  location     = {Montreal, Canada},
  pages        = {139 -- 152},
  publisher    = {ACM},
  title        = {{The benefits of relaxing punctuality}},
  doi          = {10.1145/227595.227602},
  year         = {1991},
}