USING METRIC TEMPORAL LOGIC TO SPECIFY SCHEDULING PROBLEMS
Roy Luo, Richard Valenzano, Yi Li, Christopher Beck, and Sheila McIlraith
In Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning, KR 2016
Abstract: As real-world scheduling applications diversify in scope and grow in complexity, there is an increasing need for domain-independent languages and reasoning systems that support their specification and analysis. In this paper we explore Metric Temporal Logic (MTL) as a language to support the specification of complex scheduling patterns including repeated and conditional occurrences of activities and rich temporal relationships among them. We modify the standard MTL semantics to better suit scheduling problems, and explore a series of natural restrictions to the language to gain tractability. In so doing, we provide a standard framework through which a variety of scheduling problems, from temporal networks and job shop scheduling to temporal planning, can be related and generalized. We also provide an algorithm to find a schedule specified as an MTL formula, and establish the equivalence between a fragment of MTL and simple temporal networks (STNs). Finally, we provide a proof-of-concept encoding of our scheduling language in an SMT solver, and report on experimental findings with respect to a set of illustrative examples.