Book chapter
Language Partitioning for Mission-Time Linear Temporal Logic
NASA Formal Methods, pp.313-332
Lecture Notes in Computer Science, v. 15682, Springer Nature Switzerland
2025
DOI: 10.1007/978-3-031-93706-4_18
Abstract
Mission-time Linear Temporal Logic (MLTL) is a popular variant of Linear Temporal Logic that introduces discrete, finite interval time bounds on the temporal operators. MLTL specifications reason about system behaviors encoded as finite traces that track values of key variables over time. The language of an MLTL specification is all the traces that satisfy the specification. A natural question is: Given an MLTL specification. ϕ, can we find a set of related formulas .ψ1,...,ψn so that the language of. ϕ is the disjoint union of the languages of. ψ1,...,ψn (i.e., the. ψ’s partition the language of. ϕ)? Answering this is not only theoretically interesting, but could also facilitate verification, as language partitioning is useful for creating benchmark suites or optimizing model checking algorithms. We present an algorithm for MLTL language partitioning and prove it correct. Because the proofs are technically intricate, we formalize them in the theorem prover Isabelle/HOL to ensure correctness. We automatically obtain an implementation of our algorithms via code generation from Isabelle/HOL and conduct an experimental evaluation to demonstrate the practicality of using our algorithms.
Details
- Title: Subtitle
- Language Partitioning for Mission-Time Linear Temporal Logic
- Creators
- A. E. Rosentrater - Iowa State UniversityZ. Wang - Iowa State UniversityKatherine Kosaian - University of IowaKristin Yvonne Rozier - Iowa State University
- Contributors
- Aaron Dutle (Editor)Laura Humphrey (Editor)Laura Titolo (Editor)
- Resource Type
- Book chapter
- Publication Details
- NASA Formal Methods, pp.313-332
- Publisher
- Springer Nature Switzerland; Cham
- Series
- Lecture Notes in Computer Science; v. 15682
- DOI
- 10.1007/978-3-031-93706-4_18
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 2025
- Academic Unit
- Computer Science
- Record Identifier
- 9984826346402771
Metrics
2 Record Views