Encoding Intractable Specifications via Implied Domain Constraints


We take another look at intractable temporal logic specifications, where the intractability stems from self-reference, unboundedness, or the need for explicit counting. A classic example is the specification, Every file that gets opened eventually gets closed. In all cases, we show that we can capitalize on realistic constraints implied by the operating environment to generate Mission-time Linear Temporal Logic (MLTL) encodings with reasonably-sized memory signatures. We derive a new set of rewriting rules for MLTL, accompanied by proofs of correctness for each rule, and memory optimizations. We utilize these in creating MLTL encodings for all three patterns of intractability, proving correctness, time complexity, and space complexity for each type of specification encoding.

28th International Conference on Formal Methods for Industrial Critical Systems (FMICS)