Impossible Made Possible: Encoding Intractable Specifications via Implied Domain Constraints

Chris Johannsen, Brian Kempa, Phillip H. Jones, Tichakorn Wongpiromsarn, and Kristin Yvonne Rozier

This webpage contains supplementary data for "Impossible Made Possible: Encoding Intractable Specifications via Implied Domain Constraints".

---

Abstract

We take another look at intractable temporal logic specifications, where the intractability stems from unboundedness, self-reference, 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 optimization. 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.

Supplemental Proofs

See "proofs.pdf" for full proofs of Theorems 1 and 2.