MTL with Bounded Variability: Decidability and Complexity

This paper investigates the properties of Metric Temporal Logic (MTL) over models in which time is dense but phenomena are constrained to have bounded variability. Contrary to the case of generic dense-time behaviors, MTL is proved to be fully decidable over models with bounded variability, if the variability bound is given. In these decidable cases, MTL complexity is shown to match that of simpler decidable logics such as MITL. On the contrary, MTL is undecidable if all behaviors with variability bounded by some generic constant are considered, but with an undecidability degree that is lower than in the case of generic behaviors.

• Type: Conference
• Year: 2008
• Where: FORMATS
• Authors: Carlo A. Furia, Matteo Rossi
• Keywords: Formal Methods, FORMATS 2008, Generic Dense-time Behaviors, Metric Temporal Logic, Simpler Decidable Logics