Introduction

Path planning for robotic systems is an important and challenging problem [24]. Typically, a planner is provided with the description of the robot's workspace including an initial configuration, a desired goal configuration, obstacles, and a transition relation encoding the effect of robot actions on its configurations. Most autonomous robots perform planning in a layered manner: a high-level planner first identifies a (possibly dense) sequence of way-points for the robot to follow that achieves a collision-free path through the workspace that satisfies the robot's goal. The path is then handed off to a lower-level controller that ensures that the robot's actual trajectory follows the path with minimal tracking error. While there are many planning algorithms for robots that help identify paths over finite planning horizons, specification of infinite horizon objectives and path planning for such objectives remains a significant challenge. A popular formalism to describe infinite horizon behavior of the system, such as invariance or persistence, is Linear Temporal Logic [42]. For most autonomous robots, a feasible lower-level control scheme often imposes constraints on the high-level pathstoensuredynamicfeasibility.Followingpathsthatrequireabruptchanges mayimposeunrealisticdemandsonthelow-levelcontrolthatviolateactuation constraints. Thus, producing paths that are sufficiently smooth usually makes thelow-levelcontrolproblemeasier.

Inthispaper,wetackletwochallenges:(1)generatingsmoothpathsthrough therobot'sworkspace,(2)ensuringthatthesepathscansatisfyarbitraryinfinite horizonplanningobjectivesspecifiedinLTL.Akeyobservationthatweusein ourapproachisthatforanylabeledtransitionsystemthatsatisfiesanLTL(or anyother .ω-regular)specification:ifasatisfyingpathexists,thenalasso-shaped satisfying path exists in the system. These lassos describe an infinite sequence ofsystemstatesasafiniteprefixfollowedbyaninfinitelyrepeatingfinitesuffix.

RelatedWorkonAbstraction-BasedControlSynthesis.

Thereissignificantworkonconstructingcontrollersfordynamicalsystemsthatguaranteethat theresultingclosed-loopsystemsatisfiesLinearTemporalLogic(LTL)specificationsusingapproachesfromreactivesynthesis [ 5,18,21]andabstraction-guided control [ 46,48,52]. Our approach falls under the broad category of automata based methods that model a finite state abstraction of the control system as a finite transition system [ 4,7,12,20,32,37,41,53,55,59]. These approaches use model checking [ 2,8] or other algorithms on automata to produce a satisfying lasso through the abstract transition system. However, it is challenging to map the abstract lasso to a controller of the robotic system. Additionally, it iscomputationally challenging to usethesemethods onlarge abstract systems asalgorithmsoperateontheproductoftheabstractsystemwithatranslated Büchiautomatonforthespecification,whichisexponentiallylargeinthesizeof theformula [ 2].Samplingbasedplannersaddressthisproblembyeitherincrementallybuildingasparseabstractsystemthroughsamplingsystemdynamics [4,19,35,57] or avoiding the construction of an abstract system altogether by simultaneouslyexploringthestatespaceandtranslatedBüchiautomaton [ 31].

Our Approach: Path Synthesis. Ourmethodaddressesthecomputational challengesofrelatedmethodsbysynthesizingpathsinsteadofacontroller.Relativetootherabstraction-basedmethods,wecanleverageamorecoarseabstrac-tionasinterpolatingdiscretetransitionswithaBéziersplinereducestheneedfor afine-grainedabstraction.Thiscanbeseenasanalternativetosampling-based abstract planning as both approaches seek to reduce the size of the abstract system, though our method is control-agnostic. Additionally, our method handlesinfinitehorizonpaths.Wetheoreticallyguaranteethediscretetraceofthe synthesizedpathsatisfiesanLTLspecificationandthatourmethodwillalways constructoneifsuchapathexists.However,theseguaranteesareonthesynthesized paths and extending guarantees to a controller is a challenging problem.

For thespecialcaseof differentially flat systems,wedemonstrate howexisting trajectorytrackingcontrollerscanbeusedtotracktheplannedspline.

KurtzandLin [ 23]presentthemostsimilarmethod.TheysolveforaBézier splinethatsatisfiesanLTLspecificationbyformulatingtheproblemasashortest pathprobleminagraphofconvexsets [ 33,34],whichisNP-hardbuthasatight convex relaxation. They give soundness and completeness guarantees for the synthesizedtrajectoryfortheco-safefragmentofLTLformulas,butareunable togiveacompletenessguaranteeforfullLTL.ABéziersplinethatsatisfiesthe formulamayexistwhentheirmethodfails.Wepresentanalternativemethodthat uses model checking tools to achieve soundness and completeness for full LTL. Sun et al. [ 50] present another similar method that solves for piecewise linear pathsthatsatisfyanSTLformulabyencodingthesatisfactionoftheformulaas anMILP.Althoughtheyconsidersatisfactionofadifferenttemporallogic,the Béziersplinesusedinourmethodgeneralizepiecewiselinearpaths,andunder some conditions we can translate the same problem instance into our setting. IncontrasttosolvinganNP-hardMILP,ourmethodsplitstheproblemintoa modelcheckingstepandaconvexoptimizationstep.Thissharesanexponential worst-case complexity but we demonstrate a computational advantage relative tobothofthesealternativemethods.

Contributions and Organization. Summarizingourmaincontributions:

1. Wepresentanabstraction-basedmethodthatusesmodelcheckingandconvex optimizationtoautomaticallysynthesizeaBéziersplinethatsatisfiesanLTL specification. 2. Weproveourmethodissoundandcomplete.Ourmethodwillreturnaspline thatsatisfiesthespecificationifandonlyifoneexists. 3. Wecompareourmethodagainstrecentapproachestopathsynthesis [ 23,50] and find a 5x to 1255x times computational speedup in simulated experimentsofvaryingsize. 4. Wedemonstratehowsynthesizedsplinescanbeusedinconjunctionwithtrajectorytrackingcontrollersfordifferentiallyflatsystemstosolvethecontrol synthesisproblem.

WecoverpreliminarymaterialonLTLandBéziersplinesinSect. 2.InSect. 3, we formally define our problem and describe our approach to use model checking and optimization to synthesize a Bézier spline. Section 4 presents a simulated experimental comparison with related work. In Sect.

5, we review abstractions of control systems and demonstrate how our method can be combined with trajectorytrackingcontrollersfordifferentiallyflatsystems.

Preliminaries

Linear Temporal Logic

Foramorecompletetreatment,see [ 2].LinearTemporalLogic(LTL)isaformalismthatextendspropositionallogicwithmodalitiestoexpressrequirements ontheinfinitediscretebehaviorofasystem.Defineasetofatomicpropositions .AP whichrepresentBooleanpropertiesofasystem.

Definition 1 (Syntax of LTL).ThesyntaxofLTLisasfollows.

where . T denotes "true", .a ∈ AP , . ¬ is the negation operator, . ∧ is the conjunction operator, .X is the "next" temporal operator, and

.U is the "until" temporal operator.

Othertypicalbooleanconnectors( .∨, ⇒)andtemporaloperators( .G for"globally" and .F for "eventually") are derived from the above rules.

.

and for all 0 ≤ i < j : σ[i . . .] ϕ 1 .

Thesemanticsofthederivedtemporaloperators .G and . F follow.

. σ G ϕ ⇔ for all j ≥ 0 : σ[j . . .] ϕ, σ F ϕ ⇔ exists j ≥ 0 : σ[j . . .] ϕ

The statement .σ ϕ is read as . σ "satisfies" . ϕ. Denote the set of words that satisfy . ϕ as .Words(ϕ) = {σ ∈ (2 AP ) ω | σ ϕ}.Finally,recallanyLTLformula canbetranslatedintoanon-deterministicBüchiautomaton.

Definition 3 (Büchi automaton). A non-deterministic Büchi automaton

a transition relation, and .F ⊆ Q is the acceptance set. The language .L ω (M ) is the set of infinitewordsin .(2 AP ) ω thathaveatleastoneinfiniterun .q 0 q 1 q 2 . . . in .M where .q i ∈ F forinfinitelymanyindices . i. The construction of an NBA .M ϕ where .σ ∈ Words(ϕ) iff .σ ∈ L ω (M ϕ ) takes .2 O(|ϕ|) timeandspace,yethasbeensuccessfullyappliedinmodelcheckingtools thatarecapableofhandlingmodestlysizedformulas. Definition 4 (Kripke Structure). A Kripke structure over a set of atomic propositions .AP is defined as a tuple .K = (S, I, R, h S ) where . S is a finite set of states, .I ⊆ S is a set of initial states, .R ⊆ S × S is a transition relation satisfying .∀s ∈ S, ∃s ∈ S s.t. .(s, s ) ∈ R. The function .h S : S → 2 AP is called theoutputfunctionandlabelsasetofatomicpropositionsthatholdin . S. A path through .K is an infinite sequence of states .ρ = s 1 s 2 s 3 . . . where .s 1 ∈ I and each .s i ∈ S such that for each .i ≥ 1, .(s i , s i+1 ) ∈ R. Denote .Trace(ρ) astheworddefinedbythesequenceoflabelsofeachstate

. Trace(ρ) = h S (s 1 )h S (s 2 )h S (s 3 ) . . . ∈ (2 AP ) ω . Themodel checking [ 2,8] problem decides whetherallwordsgeneratedbyaKripkestructure .K satisfyanLTLformula . ϕ. Todoso,thestandardalgorithmtakestheproductautomaton

. A := K ⊗ M ¬ϕ where .M ¬ϕ istheNBAconstructedfrom .¬ϕ andcheckswhether . A acceptsany words.Iffthelanguage .L ω (A) isempty, .K ϕ.Modelcheckersproduceawitness(orcounterexample)when .K ϕ whichisoftheform .ρ = ρ 1 (ρ 2 ) ω where .ρ 1 = s 1 . . . s n isafiniteprefixand .ρ 2 = s n+1 . . . s m isaninfinitelyrepeatedfinite suffix.Each . s i isastateintheproductautomaton

.K ⊗ M ¬ϕ whichcanbeprojectedonto . S toproduceapathof .K wheretheassociatedword .Trace(ρ) ϕ.

Bézier Splines

WeuseBéziersplinestomapdiscretewitnesses

. ρ tosmoothpaths.Béziersplines [40]areamethodofinterpolationthathavebeenusedextensivelyinthemotion planningliterature(e.g. [ 25,43,56,60]).ABéziersplineofdegree .k ∈ N isdefined bytheconcatenationofseveralcurves(orsegments)whichareeachdefinedusing aparticularsetofpolynomialbasisfunctions,theBernsteinbasispolynomials. Forsplinedegree . k, thereare .k + 1 Bernsteinbasispolynomials.

Definition 5 (Bernstein Basis Polynomial). For

.i ∈ {0, . . . , k}, the Bernsteinbasispolynomial .B i,k : [0, Δ t ] → R isdefinedby:

Where .Δ t ∈ R ++ is a strictly positive real number. Typically .Δ t = 1 but we allowtheparametertorangetoenablegreaterflexibilityonthetimingofplanned curves.WelaterrefertothefollowingpropertiesofBernsteinbasispolynomials:

Where .δ i,j istheKroneckerdeltafunctioni.e.

.δ i,j = 1 if .i = j and . 0 otherwise.A BéziercurveisdefinedusingtheBernsteinbasispolynomialsasthecoefficients ofaconvexcombinationof .k + 1 chosencontrolpoints .(p 0 , . . . , p k ) whereeach .Δ t and non-uniform otherwise. For non-uniform splines, denote the sequence of time deltas as .Δ := (Δ 1 t , . . . , Δ m t ). As each Bézier curve is a polynomial function, ensuring the spline is .C d , or .d-times continuously differentiable, amounts to checking equivalence of the first . d derivatives at the knot points. Knot points arepointswhereonecurveendsandthenextbegins.FromLemma 2,thecontrol points of the .d-th derivative are a linear function of the control points .(p 0 , . . . , p k ), so this amounts to a set of linear constraints. Corollary 1 is usefultoprovetheseconstraintsaresatisfiable.Ifthesplineisnon-uniform,these constraints are instead quadratic as the .(Δ t ) d expression is multiplied by the control points. For example, .C 1 continuity requires between the curves . j and .j + 1:

.

Path Synthesis

In this Section, we first present a formal definition of our problem, then present an algorithm that solves our problem along with formal soundness and completeness guarantees. Finally, we analyze the worst-case time complexity of our algorithm.

Problem Definition

Define the workspace .X ⊂ R n . We are given a partition .P = (P 1 , . . . , P r ) of . X into . r convex regions i.e. .P i ∩ P j = ∅ for .i = j and . i=1,...,r P i = X. Let . int(P ) and .P denote the interior and closure of the set .P respectively. We assume

.int(P ) = ∅ for each .P ∈ P. Denote the absorbing region .P * = R n \ X. We are given a set of atomic propositions

.AP and a labeling function .L : P ∪P * → 2 AP . Define .Regions(B) = P 0 P 1 . . . to be the sequence of regions . B enters where for each .i = 0, 1, . . . each .P i ∈ P and there exists a strictly increasing non-Zeno time sequence .(t 0 , t 1 , . . .) where .B(t i ) ∈ P i and there exists . i ∈ (0, t i+1t i ) where either: a. For all .t ∈ [t i , t i + i ) : B(t) ∈ P i and . t ∈ [t i + i , t i+1 ] : B(t) ∈ P i+1 b. For all .t ∈ [t i , t i + i ] : B(t) ∈ P i and . t ∈ (t i + i , t i+1 ] : B(t) ∈ P i+1

We define the trace of . B as the sequence of labels of .Regions(B). . Trace(B) := σ ∈ (2 AP ) ω where .σ = L(P 0 )L(P 1 ) . . ., .Regions(B) = P 0 P 1 . . .. Figure 1 displays an example . B. Remark 1. Requiring a convex partition is useful as constraints to require a Bézier curve remains within a convex region are convex. We assume this partition Algorithm 1:PathSynthesisfromLTLObjectives input: Partition . P,Startingstates . I, LTLformula . ϕ,Labelfunction . L 1 . K abs ← ConstructKripke(P, I, L) 2 . Mϕ ← LTLtoNBA(ϕ) 3 . ρ ← EmptinessCheck(K abs ⊗ Mϕ) 4 . B ← SynthesizeBézier(ρ) /* Check if SynthesizeBézier was feasible */ 5 if . B is not . then 6 return . B 7 return .

is given, though in practice one could be created by first taking convex overapproximations or under-approximations of labeled regions of interest in the workspace(e.g.obstacles,goalregions,etc.)andsubsequentlypartitioningthe remaining space into unlabeled convex regions. Of course this approach is not generalandprecludessomeenvironmentsfromusingourmethod,thoughweare abletoperformthisprocedureforanumberofinterestingenvironmentsusedin ourexperimentsinSects. 4 and 5.

Problem Definition. Given convex partition .P of the workspace .X ⊂ R n , labelingfunction .L : P ∪P * → 2 AP ,andanLTLspecification . ϕ over .AP , we aim tofinda .C d lassoBézierspline . B thatminimizesagivenconvexcostfunction . J suchthat .Trace(B) ϕ.

Synthesis Algorithm

Algorithm 1 details the full algorithm. ConstructKripke() constructs the Kripke structure .K abs = (S, I, R, h s ) where .S = P ∪P * , .I ⊆ S is given, .(s i , s j ) ∈ R if either .i = j or .P i ∩ P j = ∅ where .P i and .P j are the associated sets in the partition for

.s i and . s j . Finally, .h S = L is the given labeling function. We abuse notation and use

.s ∈ S to refer both to a specific Kripkestateandtheassociatedregion . P . TheLTLtoNBA() functionconstructs theNBA .M ϕ where .L ω (M ϕ ) = Words(ϕ).EmptinessCheck() performsemptiness checking, returning a witness . ρ that is accepted by .K abs ⊗ M ϕ . Practically,weconstrain . ρ tonotinclude .P * sothepathavoidstheabsorbingregion.

1 SynthesizeBézier() performsaconvexoptimizationproblemdescribedinthe followingsubsectiontoproduceaBézierspline . B where .Trace(B) = Trace(ρ). We prove SynthesizeBézier() will always be feasible if the spline order

. k is large enough, though since the problem defines constraints based on a specific witness, the resulting spline may be suboptimal as an alternative witness may producealowercostspline. TheSynthesizeBézier() functioninAlgorithm 1 solvesoneofthefollowing optimizationproblems.Givenpath .ρ = ρ 1 (ρ 2 ) ω of .K abs where .ρ 1 = s 1 . . . s l and

.ρ 2 = s l+1 . . . s m anduser-providedcostfunction .J : R k(m+1) → R, we construct a Bézier spline .B of order . k that is .d-times continuously differentiable using .m + 1 segments.Let .p j i refertothe .i-thcontrolpointofthe .j-thsegment,where .i ∈ {0, . . . , k}, and .j ∈ {1, . . . , m + 1}.Thesplineisconstructedbyminimizing:

The constraints for the .j = 1, .j = m, and .j = m + 1 curves differ slightly from theconstraints for all other curves andare separated for clarity. Aseach

.P ∈ P is convex, the constraints ( 10-17) are convex. If we require .B to be uniform,constraint( 18)islinear.Otherwise,( 18)isquadratic.Aslongas . J is a convex function, this problem can be efficiently solved to global optimality. Typical choices of cost functions include minimizing an approximation of the pathlength,orthemagnitudeofhigherorderderivativesof . B.Note . B hasone moresegmentthan .|ρ 1 ρ 2 |. Proof. Constraints ( 10-17) ensure for .j ∈ {1, . . . , m} and .i ∈ {0, . . . , k} each .p j i ∈ s j , or, .p j i ∈ P where .P istheassociatedconvexregionto . s j .Constraints ( 12),( 14), ( 17)analogouslyensure .p m+1 i ∈ s l+1 .AstheBéziercurve .b j defined bycontrolpoints .(p j 0 , . . . , p j k ) iscontainedwithintheconvexhullofthecontrol points, .∀t ∈ [0, Δ t ] : b j (t) ∈ P .Constraints( 13) and( 14)ensuresforeachspline segment . j,thereexistssome . i where .p j i ∈ int(P ). Dueto ( 2), .b j (t) for . t ∈ (0, Δ t ) is a convex combination with strictly positive weight assigned to .p j i ∈ int(P ), implying .b j (t) ∈ int(P ) forall .t ∈ (0, Δ t ). As . P isapartition, .b j (t) / ∈ P forall regions .P ∈ P, P = P forall .t ∈ (0, Δ t ).Thisholdsforall .j ∈ {1, . . . , m + 1}, therefore .Regions(B) = ρ and .Trace(B) = Trace(ρ).

The constraints of

.(P 1) are sufficient but not necessary to provide a . C d spline . B thatsatisfies .Trace(B) = Trace(ρ).Forexample,problem .(P 1) maybe infeasiblewhentherecouldexistasplinethateither(a)hasadifferentorder . k, or (b)relaxesconstraint( 13) that forevery .i ∈ {1, . . . , k -1} wehave .p j i ∈ int(s j ). For Theorem 1,weonlyusethefactthatoneof .i ∈ {1, . . . , k -1} satisfies( 13), but encoding that relaxation introduces integer variables which changes . (P 1) from a convex program to a mixed-integer convex program. Instead, simply increasingtheorder . k allowsustorelaxaconstraintandguaranteefeasibility. If .k ≥ 2d + 1,weconsiderasecondoptimizationproblem: .(P 2) : min p J(p) (20) s.t.p 1 0 ∈ s 1

j∈ {1, . . . , m}

The only changes between .(P 1) and .(P 2) is constraint ( 13) is relaxed to ( 24) and ( 25), and constraint ( 14) is relaxed to ( 26) and( 27). This is only sound when .k ≥ 2d + 1 as .{d, . . . , k -d} isnonempty.

Theorem 2 (Soundnessof .(P 2)).Givenpath . ρ of .K abs ,allfeasiblesolutions of .(P 2) produce a spline . B thatsatisfies .Trace(B) = Trace(ρ).

Proof. FollowsimmediatelyfromthesameargumentastheproofofTheorem 1.

Theassumptionsmadeon . P allowustoprove .(P 2) isfeasible.

Theorem 3 (Feasibility of .(P 2)).Givenpath . ρ of .K abs , .(P 2) isfeasible. Proof. Givenpath .ρ = ρ 1 (ρ 2 ) ω of .K abs ,weconsiderthreedistinctcasesinour construction.

• Consideringthefirstsegment .j = 1, for .i ∈ {0, . . . , k -d} pick .p 1 i tobethe same arbitrary point .x ∈ int(s 1 ). By assumption .int(P ) = ∅ for all .P ∈ P, thispointexists.For .i ∈ {kd + 1, . . . , k} pick .p 1 i tobethesamearbitrary point • Consideringthefinalsegments .j = m and .j = m + 1,theinductiveproof above showswe can make .m arbitrarilylarge,butwestillneedtoclosethe loop for the lasso spline. We construct the .m-th segment according to the previouscase,exceptfor .i ∈ {kd + 1, . . . , k} we pick . p m i = x ∈ s m ∩ s l+1 according to constraint ( 29) as .s m+1 does not exist. We pick the first . i ∈ {0, . . . , d -1} pointsofthe .m + 1 segmenttobethesamepoint .p m+1 i = x, and for .i ∈ {d, . . . , k -d} we pick .p m+1 i ∈ int(s l+1 ) to be arbitrary interior points.Fromthepreviouscase, .p l+2 i = x ∈ s l+1 ∩ s l+2 for . i ∈ {0, . . . , d -1} is some already chosen point. We pick Each point exists and has been selected according to the constraints (21)(22)(23)(24)(25)(26)(27)(28)(29)(30). As we have proven the first . d derivatives of each spline segment at .t = 0 and .t = Δ t all equal . 0, the spline is clearly .C d . Therefore, this spline also satisfies constraint ( 31)andisafeasiblesolutionof .(P 2).

In practice, we expect this construction to be high cost as it likely results inlargefluctuationsinthehigherorderderivatives,whichcanbepenalizedby sensiblechoicesofcostfunctions.However,thisconstructionguaranteeswecan alwayssynthesizea .C d spline . B for . ρ,solongaswepicklargeenough . k. Theorem 4 (CompletenessofAlgorithm 1 with .(P 2)).Algorithm 1 using .(P 2) for SynthesizeBézier() returns a Bézier spline .B with . Trace(B) = Trace(ρ).

Proof. FollowsfromTheorem 2 andTheorem 3 byselecting .k ≥ 2d + 1.

Whiletheconvexformulationallowsustofindtheoptimal

. B subjecttothe constraintsdefinedfromagivenwitness

. ρ,therecouldexistadifferentwitness .ρ or a different construction that produces a lower cost spline. Enumerating all possible witnesses may be impossible as there can be infinite. In practice, weareinterestedinasmalldiversesetofwitnessestogetanempiricallygood enoughsolutionandsimplyrandomizetheorderoftransitionsin

.K abs toproduce differentwitnesses. 2 Thischoicepreventsusfromguaranteeing . B istheoptimal spline that satisfies . ϕ, but we demonstrate in the following section it is very computationallyefficientandproducessplinesofsimilarcosttorelatedmethods.

Complexity

Focusing on the case where .(P 1) and .(P 2) admit polynomial time algorithms to minimize . J (e.g. . B is uniform, .P is a set of polyhedra, and

. J is a linear or convexquadraticfunction),thecomplexityofAlgorithm 1 isdominatedbythe modelcheckingstep,whichis .PSPACE-complete [ 2].

Proof. AnupperboundforthetimeandspacecomplexityforLTLmodelchecking can be found by translating the LTL formula into a Büchi automaton and searching for an accepting lasso, which is

Experimental Results

The following experiments were all performed using a laptop running Ubuntu 20.04 with a 16 core i7-11800H processor at 2.30 GHz, 32 GB ram, and a RTX 2080 GPU. For our method, we use the SPOT model checker [9] to produce witnesses and Gurobifoot_2 for optimization. We compare our method with [23,50] referred to as GCS for "Graph of Convex Sets" and PWL for "Piecewise Linear" respectively. Implementations of the compared methods on the experiments are provided by the respective authors. All formulas considered in this comparison are syntactically co-safe, and all splines in this section are uniform.

Numerical Comparison

Example 1 is the simple key-door problem from [23] where a planar robot must pick up both keys before passing through their associated doors in order to reach a goal. Trajectories are synthesized to satisfy the formula:

Synthesized trajectories from two different witnesses using our method are shown in Fig. 2. We ran our method and GCS for 50 trials and compared setup times, solve times, and spline costs. As both methods formulate a convex optimization problem to solve for their respective trajectories, we separate the time spent in the optimizer and all other time spent in the program into solve time and setup time. For our method, setup time includes the construction of the Kripke structure, translation of the LTL formula into a Büchi automaton, the model checking step, and setup of the convex optimization problem. For GCS, the setup time includes translation of the LTL formula into a DFA, construction of the graph of convex sets, forming a product automaton between the DFA and the graph, and setup of the convex optimization problem. In order to use the same spline parameters as presented in [23], both methods compute .C 2 splines of order .k = 3 with .Δ t = 1 and minimize the same cost function that computes the L2 norm between adjacent control points for the Bézier spline and first and second derivatives. This choice of cost function is convex, so .(P 1) and . (P 2) are convex programs for uniform splines. As .k < 2d + 1 for this experiment, we use .(P 1) for the SynthesizeBézier() calls and randomize the transition order in the Kripke structure .K abs between trials to produce different counterexamples to get a sense of how frequently .(P 1) is infeasible. Proposed GCS 0.10 0.15 0.20 0.25 0.30 0.35 0.40 0.45 0.50 Setup Time (a) Proposed GCS 0.00 0.01 0.02 0.03 0.04 0.05 0.06 0.07 Solve Time (b) Proposed GCS 0 25 50 75 100 125 150 175 200 Spline Cost (c) Fig. 4.

Comparison with [23] on Example 1. From 50 trials, our method finds a solution on average 5.1x faster and returns splines with 6.7% increased cost. 12 of the 50 trials were infeasible for .(P 1) to solve.

On average, our proposed method has significantly faster solve times but producesslightlyhighercostsplinesandhasvarianceinthecostoftheproduced spline.Thisispartiallyexplainedasourmethodalwayssolvesforalassospline whichaddsadditionalconstraintsandsegmentsrelativetothefinitetrajectory fromtheGCSmethod.Ofthesampled50trials,12wereinfeasiblefor

.(P 1) to solve.Figure 4 presentsasummaryofthiscomparison. 1. The GCS method spends significant time in setup by formulating the graph of convex sets and product automaton, which is not anon-the-flyconstructionlikeweuse.ThePWLmethodencodesthesemantics of the specification directly into the optimization problem which is a NP-hard MILP.Ourmethodavoidsboththesepitfalls.Wefindtheconstructionof

.K abs , translationof . ϕ to .M ϕ ,andthemodelcheckerrunsinlessthanhalfasecondon averagetofindawitness . ρ,andweonlyneedtoprovideasimplesetofconvex constraintstotheoptimizerthatarederivedfrom . ρ.Thisadvantageresultsina 1255xspeedupcomparedtoGCSanda370xspeedupcomparedtoPWLona sampleof50trials.Ofthe50trials,only4wereinfeasiblefor

.(P 1) tosolve.The costofthePWLmethodisincomparableasthesplineshavedifferentorderand PWL uses a different linear cost function. Compared to GCS, we observe our method on average produced splines with .16.5% higher cost but is capable of findingsplineswithlowercost.Duetothesignificantcomputationaladvantage, itispracticaltorunourmethodforseveraltrialstofindalowercostsplinein fastertime.

Scalability

To experimentally demonstrate the scalability of our method to splines with high order, we compare the performance of our method using .(P 1) and .(P 2) on Example 2. For this comparison, we solve for .C 2 splines and range the order from .k = 4 to .k = 19, minimizing the same cost function as the previous experiment. We do not run .(P 2) for .k = 4 as the order is insufficiently large for the conditions in Theorem 2 to guarantee soundness. We perform 50 random samples for each order and present the mean solve times and spline costs along with confidence intervals in Fig. 5. There is insignificant difference in the mean solve times or spline cost between our two proposed synthesis methods, which is intuitive as .(P 2) lightly relaxes some constraints of .(P 1). As the choice of . k is independent from the model checking step, the only increase in computational time is due to the convex optimization step. We observe a linear trend in the solve time, shown in (a) of Fig. 5. Intuitively, increasing . k reduces the cost of the optimal solution. Only 6 problems were infeasible for .(P 1) at .k = 4, all other problems were feasible for both methods, which is guaranteed for .(P 2) due to Theorem 3.

Dynamic Feasibility and Trajectory Tracking

While our method provides a path that achieves a specification, the path may not be dynamically feasible for a specific control system and it is not trivial to design a controller that tracks the path. Moreover, model uncertainty, disturbances, and state estimation errors introduce additional error where the online execution of a synthesized path may now actually violate the specification. This caveat is important to highlight, our soundness and completeness guarantees are with respect to the path and extending those guarantees to a controller is a significantly challenging problem. These issues motivate the usage of sophisticated trajectory tracking controllers to execute planned splines. convex actuator constraints could map to non-convex regions in the flat output space, including constraints on . u typically requires conservatively bounding derivatives [14]. This differential flatness approach is popular to plan trajectories for quadrotors (e.g. [10,36,45,49]). A.C ν curve planned in the flat output space is a dynamically feasible trajectory, but to handle model uncertainty, disturbances, and tracking errors, these methods combine with a trajectory tracking controller where many methods have been studied such as model predictive control (MPC) [1,11,51] and geometric control [26,27]. In this way, our method can plan reference paths in the flat output space while a trajectory tracking controller for the control system of interest can be used to track the planned path.

Quadrotor Trajectory Tracking. We use a simple model of quadrotor dynamics without disturbances or drag, the same presented in [36]. Recall from Sect. 2.2, the constraints to impose velocity and acceleration limits are linear for uniform splines . B. We leverage the controller from [27] to track the reference paths. We plan the reference Bézier spline . B in the flat output space .z = (x, ψ) where . x is the 3D position and . ψ is the yaw angle of the quadrotor. . B is planned to satisfy .ϕ = G F(blue) ∧ G F(green) ∧ G(¬red). The transformations . β and . γ from the flat output space to the state and control spaces of the quadrotor requires . x to be .C 5 and . ψ to be .C 3 , so we set .d = 5 and .k = 11 and use .(P 2). We constrain the reference spline acceleration to be below 1.5 m/s. 2 and velocity to be below 2.5 m/s. These additional constraints means Theorem 3 does not apply, though empirically we did not encounter any infeasible problems when running this experiment. Planned and executed trajectories that drive the quadrotor twice around the looping section in . B are displayed in Fig. 6, along with the trajectory trackingerror.Noteeachregionisunboundedinthe

. z axisbutpresentedasa 2Dregionforclarity.Theoverallplanningtimeforthisproblemis0.75s.

Related Work

Apopularmethodtosynthesizecontrollersfordiscretetimesystemsistoformulatesatisfactionofthetemporallogicobjectiveasamixedintegerlinearprogram (MILP) [ 3,6,44,47]. This approach has been extended for multi-agent systems [50].AdrawbackofthisapproachistheNP-hardnessoftheMILP.Additional binaryvariablesareaddedastheproblemhorizonincreases,makingscalingto longhorizonsandmulti-agentsystemsdifficult,andentirelyprohibitinginfinite horizontrajectories.Additionally,MILPapproachesrequirelinearorlinearized dynamics and the MILP often does not encode information about the system trajectory between discrete waypoints. Guaranteeing satisfaction of a continuous time system from a discrete time sampled trajectory requires additional reasoningbye.g.strictification [ 13]ortrajectoryparameterizations [ 50].

Optimizationandcontrolsmethodshavebeenusedtodirectlyoptimizethe robustness of a Signal Temporal Logic (STL) objective by defining smooth approximationsoftherobustnessmetric [ 16,17,38],whichcanbeincorporated into automatic differentiation systems [ 28]. Methods in this category either directly optimize a parameterized version of the trajectory [ 39], or formulate anoptimalcontrolproblemtomaximizeasmoothrobustnessbyadaptingalgorithms like SQP [ 16,38] and DDP [ 22]. This approach also requires finite time satisfactionoftheformula,andthesmoothrobustnesssemanticsarenon-convex sothesemethodscanonlyguaranteelocaloptimality.Controlbarrierfunctions (CBF)forafragmentofSTLhavebeenstudiedin [ 29,30]whichguaranteecontinuous time satisfaction with control actions that can be solved with convex programming.ThismethodalleviatesthecomputationalchallengeoftheMILP andoptimizationbasedapproaches,butmustrelyonexpertknowledgetodesign appropriateCBFsforeachformula,andonlyappliestoarestrictedfragmentof STL.

Conclusion

We have presented a sound and complete method that synthesizes a smooth pathwhichautomaticallysatisfiesanLTLformula.Additionally,wehavedemonstrated a significant computational advantage on benchmark problems relative toexistingwork.Inthefuture,weplanonextendingformalguaranteestotrajectory tracking controllers, as well as extending our method to multi-agent systems.