2012 19th International Symposium on Temporal Representation and Reasoning (TIME) (2012)
Sept. 12, 2012 to Sept. 14, 2012
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2012.22
Many industrial systems include components interacting with each other that evolve with possibly very different speeds. To deal with this situation many formalisms adopt the abstraction of ``zero-time transitions'', which do not consume time. These, however, have several drawbacks in terms of naturalness and logic consistency, as a system is modeled to be in different states at the same time. We introduce a metric temporal logic, called X-TRIO, that uses non-standard analysis to elegantly deal with zero-time transitions in an abstract, descriptive way. We study the decidability of the logic, and we introduce a decision procedure for a subset thereof. X-TRIO has been applied in companion works to the design and verification of industrial systems.
L. Ferrucci, D. Mandrioli, A. Morzenti and M. Rossi, "A Metric Temporal Logic for Dealing with Zero-Time Transitions," 2012 19th International Symposium on Temporal Representation and Reasoning (TIME), Leicester, 2012, pp. 81-88.