کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4951970 | 1441998 | 2017 | 28 صفحه PDF | دانلود رایگان |
- A rich timed specification language, Time Window Temporal Logic (TWTL), is proposed.
- A notion of temporal relaxation of TWTL formulae is proposed.
- A framework to translate TWTL formulae to annotated finite automata is proposed.
- Algorithms for synthesis, verification, and parameter learning are proposed.
- The algorithms' complexity is independent of deadlines due to the annotated automata.
This paper introduces time window temporal logic (TWTL), a rich expressive language for describing various time bounded specifications. In particular, the syntax and semantics of TWTL enable the compact representation of serial tasks, which are prevalent in various applications including robotics, sensor systems, and manufacturing systems. This paper also discusses the relaxation of TWTL formulae with respect to the deadlines of the tasks. Efficient automata-based frameworks are presented to solve synthesis, verification and learning problems. The key ingredient to the presented solution is an algorithm to translate a TWTL formula to an annotated finite state automaton that encodes all possible temporal relaxations of the given formula. Some case studies are presented to illustrate the expressivity of the logic and the proposed algorithms.
Journal: Theoretical Computer Science - Volume 691, 29 August 2017, Pages 27-54