Sampling polynomial trajectories for LTL verification

Daniel Selvaratnam*, Michael Cantoni, J. M. Davoren, Iman Shames

*Corresponding author for this work

    Research output: Contribution to journalArticlepeer-review

    2 Citations (Scopus)

    Abstract

    This paper concerns the verification of continuous-time polynomial spline trajectories against linear temporal logic specifications (LTL without ‘next’). Each atomic proposition is assumed to represent a state space region described by a multivariate polynomial inequality. The proposed approach samples a trajectory strategically, to capture every one of its region transitions. This yields a discrete word called a trace, which is amenable to established formal methods for path checking. The original continuous-time trajectory is shown to satisfy the specification if and only if its trace does. General topological conditions on the sample points are derived that ensure a trace is recorded for arbitrary continuous paths, given arbitrary region descriptions. Using techniques from computer algebra, a trace generation algorithm is developed to satisfy these conditions when the path and region boundaries are defined by polynomials. The proposed POLYTRACE algorithm has polynomial complexity in the number of atomic propositions, and is guaranteed to produce a trace of any polynomial path. Its performance is demonstrated via numerical examples and a case study from robotics.

    Original languageEnglish
    Pages (from-to)135-163
    Number of pages29
    JournalTheoretical Computer Science
    Volume897
    DOIs
    Publication statusPublished - 2 Jan 2022

    Fingerprint

    Dive into the research topics of 'Sampling polynomial trajectories for LTL verification'. Together they form a unique fingerprint.

    Cite this