MSO logics for weighted timed automata

作者：Quaas Karin^*

来源：Formal Methods in System Design, 2011, 38(3): 193-222.

DOI：10.1007/s10703-011-0112-6

• Weighted timed automata
• Weighted MSO logic
• Real-time systems

We aim to generalize Buchi's fundamental theorem on the coincidence of recognizable and MSO-definable languages to a weighted timed setting. For this, we investigate weighted timed automata and show how we can extend Wilke's relative distance logic with weights taken from an arbitrary semiring. We show that every formula in our logic can effectively be transformed into a weighted timed automaton, and vice versa. The results indicate the robustness of weighted timed automata and may also be used for specification purposes.

• 出版日期2011-6