Optimal Secure Control with Linear Temporal Logic Constraints

Andrew Clark; Luyao Niu

arxiv: 1907.07556 · v1 · pith:S6YH525Ynew · submitted 2019-07-17 · 📡 eess.SY · cs.SY

Optimal Secure Control with Linear Temporal Logic Constraints

Luyao Niu , Andrew Clark This is my paper

Pith reviewed 2026-05-24 20:20 UTC · model grok-4.3

classification 📡 eess.SY cs.SY

keywords linear temporal logicstochastic gamessecure controlvalue iterationpolicy iterationcyber-physical systemsadversarial attacksrobust control synthesis

0 comments

The pith

Value iteration computes the control policy maximizing LTL satisfaction probability in a stochastic game where the adversary observes the policy first.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper models a discrete-time dynamical system subject to an LTL constraint and a malicious adversary as a stochastic game in which the adversary sees the controller's policy before selecting its attack. It develops a value iteration algorithm that finds the policy achieving the highest probability of satisfying the LTL formula under this information structure. For the subclass of specifications that combine an arbitrary LTL formula with an invariant, a policy iteration algorithm additionally minimizes the expected number of invariant violations while preserving the LTL objective. These constructions address the design of controllers for cyber-physical systems that must remain functional against deliberate attacks.

Core claim

The authors model the controller-adversary interaction as a stochastic game and show that value iteration yields the optimal policy maximizing the probability of LTL satisfaction. For LTL formulas augmented by an invariant constraint they characterize the optimality condition and give a policy iteration procedure that jointly maximizes LTL satisfaction probability while minimizing expected invariant violations.

What carries the argument

Stochastic game between the controller and the policy-aware adversary, solved by value iteration for the general LTL case and policy iteration for the invariant-augmented case.

If this is right

The computed policy is optimal against any attack chosen with full knowledge of the policy.
The value iteration procedure terminates with the maximal achievable satisfaction probability for any finite-state system and LTL formula.
For the subclass problem the policy iteration algorithm returns a policy that achieves the stated optimality tradeoff between LTL satisfaction and invariant violations.
Both algorithms apply directly to any discrete-time system whose state space admits a finite abstraction compatible with the LTL specification.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The modeling choice of policy observation by the adversary could be relaxed to partial observation while retaining similar algorithmic structure.
The same game formulation might be used to compare the cost of security against different information patterns available to the attacker.
Numerical case studies in the paper indicate that the methods scale to moderate-sized systems arising in networked control.

Load-bearing premise

The adversary observes the control policy before choosing an attack strategy.

What would settle it

Enumeration of all policies on a small finite-state stochastic game instance yields a strictly higher LTL satisfaction probability than the policy returned by the value iteration algorithm.

Figures

Figures reproduced from arXiv: 1907.07556 by Andrew Clark, Luyao Niu.

**Figure 1.** Figure 1: Comparison of the proposed approach and the approach without considering the presence of the adversary. Fig. 1a gives [PITH_FULL_IMAGE:figures/full_fig_p014_1.png] view at source ↗

**Figure 2.** Figure 2: Comparison of the proposed approach and the approach without considering the presence of the adversary. Fig. 1a gives [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗

read the original abstract

Prior work on automatic control synthesis for cyber-physical systems under logical constraints has primarily focused on environmental disturbances or modeling uncertainties, however, the impact of deliberate and malicious attacks has been less studied. In this paper, we consider a discrete-time dynamical system with a linear temporal logic (LTL) constraint in the presence of an adversary, which is modeled as a stochastic game. We assume that the adversary observes the control policy before choosing an attack strategy. We investigate two problems. In the first problem, we synthesize a robust control policy for the stochastic game that maximizes the probability of satisfying the LTL constraint. A value iteration based algorithm is proposed to compute the optimal control policy. In the second problem, we focus on a subclass of LTL constraints, which consist of an arbitrary LTL formula and an invariant constraint. We then investigate the problem of computing a control policy that minimizes the expected number of invariant constraint violations while maximizing the probability of satisfying the arbitrary LTL constraint. We characterize the optimality condition for the desired control policy. A policy iteration based algorithm is proposed to compute the control policy. We illustrate the proposed approaches using two numerical case studies.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Paper gives value and policy iteration for LTL satisfaction in a Stackelberg stochastic game where the adversary sees the policy first.

read the letter

The main takeaway is that this paper formulates secure control under LTL constraints as a stochastic game where the adversary observes the controller's policy first, then gives value iteration for maximizing satisfaction probability and policy iteration for a combined objective with invariants. It does a clean job of identifying the gap: most prior LTL synthesis handles disturbances or uncertainty, but deliberate attacks have received less attention. The algorithms follow the usual product construction with the Büchi automaton and then apply standard dynamic programming on the resulting game. The optimality condition for the second problem is stated explicitly, which aligns with results from constrained stochastic games. The modeling choice is laid out clearly in the abstract, so there is no hidden assumption that undermines the claims. The stress test found no internal inconsistency in the stated approach. One limitation is that everything rests on the full-information Stackelberg setup. If the adversary has only partial observations, the problem changes and the current algorithms would not apply directly. The numerical case studies are mentioned but their details are not in the abstract, so it is difficult to assess practical performance. This paper is for people in control theory and formal methods who work on safety-critical systems with security requirements. A reader already familiar with LTL synthesis in MDPs will see the extension without much trouble. It is worth sending to peer review because the problem formulation is timely and the algorithmic contribution is a direct, reproducible extension of existing methods.

Referee Report

0 major / 2 minor

Summary. The paper studies secure control synthesis for discrete-time dynamical systems subject to LTL constraints under adversarial attacks, modeled as a stochastic game in which the adversary observes the control policy before choosing its strategy (a Stackelberg formulation). Two problems are addressed: (1) synthesis of a policy maximizing the probability of LTL satisfaction, solved via a value-iteration algorithm on the product construction; (2) for the subclass consisting of an arbitrary LTL formula plus an invariant constraint, synthesis of a policy that minimizes expected invariant violations while maximizing LTL satisfaction probability, solved via a policy-iteration algorithm after characterizing an optimality condition. The methods are illustrated on two numerical case studies.

Significance. If the algorithms and optimality condition are correctly derived, the work extends standard LTL synthesis techniques (product automata, dynamic programming) to adversarial Stackelberg stochastic games, which is a natural and relevant direction for secure cyber-physical systems. Credit is due for cleanly separating the two problem variants and for grounding the second problem in an explicit optimality condition rather than a heuristic trade-off.

minor comments (2)

The abstract states that the adversary 'observes the control policy before choosing an attack strategy' but does not indicate where in the manuscript the justification for this modeling choice (versus a simultaneous-move game) is discussed; a brief paragraph contrasting the two formulations would improve clarity.
The description of the numerical case studies is limited to the statement that they 'illustrate the proposed approaches'; adding a short table or paragraph summarizing the system dimensions, LTL formulas used, and achieved probabilities would help readers assess practical relevance without needing to consult the full figures.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive review, accurate summary of our contributions, and recommendation for minor revision. The assessment correctly identifies the extension of LTL synthesis techniques to Stackelberg stochastic games and the separation of the two problem variants.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper models the problem as a Stackelberg stochastic game where the adversary observes the policy first, then proposes standard value iteration on the product automaton to maximize LTL satisfaction probability and policy iteration for the invariant+LTL subclass. These are direct applications of known dynamic programming methods for constrained stochastic games; no equation reduces a claimed prediction to a fitted parameter by construction, no self-citation is invoked as a uniqueness theorem that forces the result, and the optimality conditions are characterized from the game definition rather than smuggled in via prior work by the same authors. The derivation chain is self-contained against external benchmarks for stochastic-game value functions.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Review performed on abstract only; ledger therefore limited to modeling choices stated in the abstract. No free parameters or invented entities are described.

axioms (2)

domain assumption The interaction is modeled as a stochastic game in which the adversary observes the control policy before selecting its attack.
Central modeling premise stated in the abstract.
domain assumption The system is a discrete-time dynamical system subject to an LTL constraint.
Stated as the problem setting in the abstract.

pith-pipeline@v0.9.0 · 5724 in / 1017 out tokens · 30824 ms · 2026-05-24T20:20:04.574206+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We assume that the adversary observes the control policy before choosing an attack strategy... value iteration based algorithm... policy iteration based algorithm
IndisputableMonolith/Foundation/DimensionForcing.lean alexander_duality_circle_linking unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Generalized Accepting Maximal End Component (GAMEC)... reachability probability

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

47 extracted references · 47 canonical work pages

[1]

Temporal logic motion planning and control with probabilistic satisfaction guarantees,

M. Lahijanian, S. B. Andersson, and C. Belta, “Temporal logic motion planning and control with probabilistic satisfaction guarantees,” IEEE Transactions on Robotics , vol. 28, no. 2, pp. 396–409, 2012

work page 2012
[2]

Safe control under uncertainty with proba- bilistic signal temporal logic,

D. Sadigh and A. Kapoor, “Safe control under uncertainty with proba- bilistic signal temporal logic,” in Robotics: Science and Systems , 2016

work page 2016
[3]

Receding horizon temporal logic planning for dynamical systems,

T. Wongpiromsarn, U. Topcu, and R. M. Murray, “Receding horizon temporal logic planning for dynamical systems,” in the Proc. of the 48th IEEE Conf. on Decision and Control (CDC) , 2009, pp. 5997–6004

work page 2009
[4]

Sampling-based motion planning with deterministic µ-calculus speciﬁcations,

S. Karaman and E. Frazzoli, “Sampling-based motion planning with deterministic µ-calculus speciﬁcations,” in the Proc. of the 48th IEEE Conf. on Decision and Control (CDC) , 2009, pp. 2222–2229

work page 2009
[5]

Automatic synthesis of multi- agent motion tasks based on LTL speciﬁcations,

S. G. Loizou and K. J. Kyriakopoulos, “Automatic synthesis of multi- agent motion tasks based on LTL speciﬁcations,” inthe Proc. of the 43rd IEEE Conf. on Decision and Control (CDC) , vol. 1, 2004, pp. 153–158

work page 2004
[6]

Baier, J.-P

C. Baier, J.-P. Katoen, and K. G. Larsen, Principles of Model Checking . MIT Press, 2008

work page 2008
[7]

Veriﬁcation and refutation of probabilistic speciﬁcations via games,

M. Kattenbelt and M. Huth, “Veriﬁcation and refutation of probabilistic speciﬁcations via games,” in IARCS Annual Conf. on Foundations of Software Technology and Theoretical Computer Science . Schloss Dagstuhl-Leibniz-Zentrum f ¨ur Informatik, 2009

work page 2009
[8]

Robust control of uncertain Markov decision processes with temporal logic speciﬁcations,

E. M. Wolff, U. Topcu, and R. M. Murray, “Robust control of uncertain Markov decision processes with temporal logic speciﬁcations,” in the Proc. of the 51st IEEE Conf. on Decision and Control (CDC) , 2012, pp. 3372–3379. 16

work page 2012
[9]

Optimal control of Markov decision processes with linear temporal logic constraints,

X. Ding, S. L. Smith, C. Belta, and D. Rus, “Optimal control of Markov decision processes with linear temporal logic constraints,” IEEE Transactions on Automatic Control, vol. 59, no. 5, pp. 1244–1257, 2014

work page 2014
[10]

CIA Report: Cyber extortionists attacked foreign power grid, disrupting delivery,

K. O’Connell, “CIA Report: Cyber extortionists attacked foreign power grid, disrupting delivery,” http://www.ibls.com/internet law news portal view.aspx?id=1963&s=latestnews

work page 1963
[11]

Experimental security analysis of a modern automobile,

K. Koscher, A. Czeskis, F. Roesner, S. Patel, T. Kohno, S. Checkoway, D. McCoy, B. Kantor, D. Anderson, H. Shacham, and S. Savage, “Experimental security analysis of a modern automobile,” in IEEE Symp. on Security and Privacy , 2010, pp. 447–462

work page 2010
[12]

Unmanned aircraft capture and control via GPS spooﬁng,

A. J. Kerns, D. P. Shepard, J. A. Bhatti, and T. E. Humphreys, “Unmanned aircraft capture and control via GPS spooﬁng,” Journal of Field Robotics, vol. 31, no. 4, pp. 617–636, 2014

work page 2014
[13]

Playing games for security: An efﬁcient exact algorithm for solving Bayesian Stackelberg games,

P. Paruchuri, J. P. Pearce, J. Marecki, M. Tambe, F. Ordonez, and S. Kraus, “Playing games for security: An efﬁcient exact algorithm for solving Bayesian Stackelberg games,” in Proc. of the Intl. Conf. on Autonomous agents and multiagent systems . International Foundation for Autonomous Agents and Multiagent Systems, 2008, pp. 895–902

work page 2008
[14]

Stackelberg-game analysis of correlated attacks in cyber-physical systems,

M. Zhu and S. Martinez, “Stackelberg-game analysis of correlated attacks in cyber-physical systems,” in the Proc. of American Control Conf. IEEE, 2011, pp. 4063–4068

work page 2011
[15]

Patrolling security games: Deﬁnition and algorithms for solving large instances with single patroller and single intruder,

N. Basilico, N. Gatti, and F. Amigoni, “Patrolling security games: Deﬁnition and algorithms for solving large instances with single patroller and single intruder,” Artiﬁcial Intelligence, vol. 184, pp. 78–123, 2012

work page 2012
[16]

Tambe, Security and Game Theory: Algorithms, Deployed Systems, Lessons Learned

M. Tambe, Security and Game Theory: Algorithms, Deployed Systems, Lessons Learned. Cambridge University Press, 2011

work page 2011
[17]

Prism-games: A model checker for stochastic multi-player games

T. Chen, V . Forejt, M. Z. Kwiatkowska, D. Parker, and A. Simaitis, “Prism-games: A model checker for stochastic multi-player games.” in the Proc. of Intl. Conf. on TACAS . Springer, 2013, pp. 185–191

work page 2013
[18]

A stochastic games framework for veriﬁcation and control of discrete time stochastic hybrid systems,

J. Ding, M. Kamgarpour, S. Summers, A. Abate, J. Lygeros, and C. Tomlin, “A stochastic games framework for veriﬁcation and control of discrete time stochastic hybrid systems,” Automatica, vol. 49, no. 9, pp. 2665–2674, 2013

work page 2013
[19]

Where’s Waldo? sensor-based temporal logic motion planning,

H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas, “Where’s Waldo? sensor-based temporal logic motion planning,” in the Proc. of IEEE Intl. Conf. on Robotics and Automation , 2007, pp. 3116–3121

work page 2007
[20]

Sampling-based motion planning with temporal goals,

A. Bhatia, L. E. Kavraki, and M. Y . Vardi, “Sampling-based motion planning with temporal goals,” in the Proc. of IEEE Intl. Conf. on Robotics and Automation , 2010, pp. 2689–2696

work page 2010
[21]

Motion planning with dynamics by a synergistic combination of layers of planning,

E. Plaku, L. E. Kavraki, and M. Y . Vardi, “Motion planning with dynamics by a synergistic combination of layers of planning,” IEEE Transactions on Robotics , vol. 26, no. 3, pp. 469–482, 2010

work page 2010
[22]

Optimal temporal logic planning in probabilistic semantic maps,

J. Fu, N. Atanasov, U. Topcu, and G. J. Pappas, “Optimal temporal logic planning in probabilistic semantic maps,” in the Proc. of IEEE Intl. Conf. on Robotics and Automation , 2016, pp. 3690–3697

work page 2016
[23]

Motion planning and control from temporal logic speciﬁcations with probabilis- tic satisfaction guarantees,

M. Lahijanian, J. Wasniewski, S. B. Andersson, and C. Belta, “Motion planning and control from temporal logic speciﬁcations with probabilis- tic satisfaction guarantees,” in the Proc. of IEEE Intl. Conf. on Robotics and Automation, 2010, pp. 3227–3232

work page 2010
[24]

A fully automated framework for control of linear systems from temporal logic speciﬁcations,

M. Kloetzer and C. Belta, “A fully automated framework for control of linear systems from temporal logic speciﬁcations,” IEEE Transactions on Automatic Control , vol. 53, no. 1, pp. 287–297, 2008

work page 2008
[25]

Synthesis of shared autonomy policies with tem- poral logic speciﬁcations,

J. Fu and U. Topcu, “Synthesis of shared autonomy policies with tem- poral logic speciﬁcations,” IEEE Transactions on Automation Science and Engineering, vol. 13, no. 1, pp. 7–17, 2016

work page 2016
[26]

Analyzing unsynthesizable speciﬁcations for high-level robot behavior using LTLMoP,

V . Raman and H. Kress-Gazit, “Analyzing unsynthesizable speciﬁcations for high-level robot behavior using LTLMoP,” in Computer Aided Veriﬁcation. Springer, 2011, pp. 663–668

work page 2011
[27]

Minimum-violation LTL planning with conﬂicting speciﬁcations,

J. Tumov ´a, L. I. R. Castro, S. Karaman, E. Frazzoli, and D. Rus, “Minimum-violation LTL planning with conﬂicting speciﬁcations,” in the Proc. of American Control Conf. IEEE, 2013, pp. 200–205

work page 2013
[28]

Robust control of Markov decision pro- cesses with uncertain transition matrices,

A. Nilim and L. El Ghaoui, “Robust control of Markov decision pro- cesses with uncertain transition matrices,” Operations Research, vol. 53, no. 5, pp. 780–798, 2005

work page 2005
[29]

Synthesis of joint control and active sensing strategies under temporal logic constraints,

J. Fu and U. Topcu, “Synthesis of joint control and active sensing strategies under temporal logic constraints,” IEEE Transactions on Automatic Control, vol. 61, no. 11, pp. 3464–3476, 2016

work page 2016
[30]

Fudenberg and J

D. Fudenberg and J. Tirole, Game Theory. MIT Press, 1991

work page 1991
[31]

Parameter synthesis for Markov models: Faster than ever,

T. Quatmann, C. Dehnert, N. Jansen, S. Junges, and J.-P. Katoen, “Parameter synthesis for Markov models: Faster than ever,” inIntl. Symp. on Automated Technology for Veriﬁcation and Analysis. Springer, 2016, pp. 50–67

work page 2016
[32]

A game- based abstraction-reﬁnement framework for Markov decision processes,

M. Kattenbelt, M. Kwiatkowska, G. Norman, and D. Parker, “A game- based abstraction-reﬁnement framework for Markov decision processes,” Formal Methods in System Design , vol. 36, no. 3, pp. 246–280, 2010

work page 2010
[33]

Concurrent omega-regular games,

L. de Alfaro and T. A. Henzinger, “Concurrent omega-regular games,” in Proc. of IEEE symp. on Logic in Computer Science , 2000, pp. 141–154

work page 2000
[34]

A game theoretic study of attack and defense in cyber-physical systems,

C. Y . Ma, N. S. Rao, and D. K. Yau, “A game theoretic study of attack and defense in cyber-physical systems,” in the Proc. of IEEE Conf. on Computer Communications Workshops, 2011, pp. 708–713

work page 2011
[35]

Jamming attacks on remote state estimation in cyber-physical systems: A game-theoretic approach,

Y . Li, L. Shi, P. Cheng, J. Chen, and D. E. Quevedo, “Jamming attacks on remote state estimation in cyber-physical systems: A game-theoretic approach,” IEEE Transactions on Automatic Control , vol. 60, no. 10, pp. 2831–2836, 2015

work page 2015
[36]

Stackelberg vs. Nash in security games: An extended investigation of interchangeability, equivalence, and uniqueness,

D. Korzhyk, Z. Yin, C. Kiekintveld, V . Conitzer, and M. Tambe, “Stackelberg vs. Nash in security games: An extended investigation of interchangeability, equivalence, and uniqueness,” Journal of Artiﬁcial Intelligence Research, vol. 41, no. 2, pp. 297–327, 2011

work page 2011
[37]

Secure control under linear temporal logic constraints

L. Niu and A. Clark, “Secure control under linear temporal logic constraints.” in the Proc. of American Control Conf. IEEE, 2018

work page 2018
[38]

Event-triggered state observers for sparse sensor noise/attacks,

Y . Shoukry and P. Tabuada, “Event-triggered state observers for sparse sensor noise/attacks,” IEEE Transactions on Automatic Control, vol. 61, no. 8, pp. 2079–2091, 2016

work page 2079
[39]

Secure estimation and control for cyber-physical systems under adversarial attacks,

H. Fawzi, P. Tabuada, and S. Diggavi, “Secure estimation and control for cyber-physical systems under adversarial attacks,” IEEE Transactions on Automatic Control, vol. 59, no. 6, pp. 1454–1467, 2014

work page 2014
[40]

Game theory meets network security and privacy,

M. H. Manshaei, Q. Zhu, T. Alpcan, T. Bacs ¸ar, and J.-P. Hubaux, “Game theory meets network security and privacy,” ACM Computing Surveys , vol. 45, no. 3, p. 25, 2013

work page 2013
[41]

Game-theoretic methods for robustness, security, and resilience of cyberphysical control systems: games-in-games prin- ciple for optimal cross-layer resilient control systems,

Q. Zhu and T. Basar, “Game-theoretic methods for robustness, security, and resilience of cyberphysical control systems: games-in-games prin- ciple for optimal cross-layer resilient control systems,” IEEE Control Systems Magazine, vol. 35, no. 1, pp. 46–65, 2015

work page 2015
[42]

Robust and resilient control design for cyber- physical systems with an application to power systems,

Q. Zhu and T. Bas ¸ar, “Robust and resilient control design for cyber- physical systems with an application to power systems,” in the Proc. of the 50th IEEE Conf. on Decision and Control and European Control Conf., 2011, pp. 4066–4071

work page 2011
[43]

D. P. Bertsekas, D. P. Bertsekas, D. P. Bertsekas, and D. P. Bertsekas, Dynamic Programming and Optimal Control . Athena Scientiﬁc Bel- mont, MA, 1995, vol. 1, no. 2

work page 1995
[44]

A probabilistic approach for control of a stochastic system from LTL speciﬁcations,

M. Lahijanian, S. B. Andersson, and C. Belta, “A probabilistic approach for control of a stochastic system from LTL speciﬁcations,” in the Proc. of the 48th IEEE Conf. on Decision and Control/Chinese Control Conf. , 2009, pp. 2236–2241

work page 2009
[45]

An overview of existing methods and recent advances in sequential monte carlo,

O. Capp ´e, S. J. Godsill, and E. Moulines, “An overview of existing methods and recent advances in sequential monte carlo,” Proceedings of the IEEE , vol. 95, no. 5, pp. 899–924, 2007

work page 2007
[46]

Zur theorie der gesellschaftsspiele,

J. v. Neumann, “Zur theorie der gesellschaftsspiele,” Mathematische annalen, vol. 100, no. 1, pp. 295–320, 1928

work page 1928
[47]

Hogben, Handbook of Linear Algebra

L. Hogben, Handbook of Linear Algebra . Chapman and Hall/CRC, 2013. Luyao Niu (SM’15) received the B.Eng. degree from the School of Electro-Mechanical Engineering, Xidian University, Xian, China, in 2013 and the M.Sc. degree from the Department of Electrical and Computer Engineering, Worcester Polytechnic Insti- tute (WPI) in 2015. He has been working tow...

work page 2013

[1] [1]

Temporal logic motion planning and control with probabilistic satisfaction guarantees,

M. Lahijanian, S. B. Andersson, and C. Belta, “Temporal logic motion planning and control with probabilistic satisfaction guarantees,” IEEE Transactions on Robotics , vol. 28, no. 2, pp. 396–409, 2012

work page 2012

[2] [2]

Safe control under uncertainty with proba- bilistic signal temporal logic,

D. Sadigh and A. Kapoor, “Safe control under uncertainty with proba- bilistic signal temporal logic,” in Robotics: Science and Systems , 2016

work page 2016

[3] [3]

Receding horizon temporal logic planning for dynamical systems,

T. Wongpiromsarn, U. Topcu, and R. M. Murray, “Receding horizon temporal logic planning for dynamical systems,” in the Proc. of the 48th IEEE Conf. on Decision and Control (CDC) , 2009, pp. 5997–6004

work page 2009

[4] [4]

Sampling-based motion planning with deterministic µ-calculus speciﬁcations,

S. Karaman and E. Frazzoli, “Sampling-based motion planning with deterministic µ-calculus speciﬁcations,” in the Proc. of the 48th IEEE Conf. on Decision and Control (CDC) , 2009, pp. 2222–2229

work page 2009

[5] [5]

Automatic synthesis of multi- agent motion tasks based on LTL speciﬁcations,

S. G. Loizou and K. J. Kyriakopoulos, “Automatic synthesis of multi- agent motion tasks based on LTL speciﬁcations,” inthe Proc. of the 43rd IEEE Conf. on Decision and Control (CDC) , vol. 1, 2004, pp. 153–158

work page 2004

[6] [6]

Baier, J.-P

C. Baier, J.-P. Katoen, and K. G. Larsen, Principles of Model Checking . MIT Press, 2008

work page 2008

[7] [7]

Veriﬁcation and refutation of probabilistic speciﬁcations via games,

M. Kattenbelt and M. Huth, “Veriﬁcation and refutation of probabilistic speciﬁcations via games,” in IARCS Annual Conf. on Foundations of Software Technology and Theoretical Computer Science . Schloss Dagstuhl-Leibniz-Zentrum f ¨ur Informatik, 2009

work page 2009

[8] [8]

Robust control of uncertain Markov decision processes with temporal logic speciﬁcations,

E. M. Wolff, U. Topcu, and R. M. Murray, “Robust control of uncertain Markov decision processes with temporal logic speciﬁcations,” in the Proc. of the 51st IEEE Conf. on Decision and Control (CDC) , 2012, pp. 3372–3379. 16

work page 2012

[9] [9]

Optimal control of Markov decision processes with linear temporal logic constraints,

X. Ding, S. L. Smith, C. Belta, and D. Rus, “Optimal control of Markov decision processes with linear temporal logic constraints,” IEEE Transactions on Automatic Control, vol. 59, no. 5, pp. 1244–1257, 2014

work page 2014

[10] [10]

CIA Report: Cyber extortionists attacked foreign power grid, disrupting delivery,

K. O’Connell, “CIA Report: Cyber extortionists attacked foreign power grid, disrupting delivery,” http://www.ibls.com/internet law news portal view.aspx?id=1963&s=latestnews

work page 1963

[11] [11]

Experimental security analysis of a modern automobile,

K. Koscher, A. Czeskis, F. Roesner, S. Patel, T. Kohno, S. Checkoway, D. McCoy, B. Kantor, D. Anderson, H. Shacham, and S. Savage, “Experimental security analysis of a modern automobile,” in IEEE Symp. on Security and Privacy , 2010, pp. 447–462

work page 2010

[12] [12]

Unmanned aircraft capture and control via GPS spooﬁng,

A. J. Kerns, D. P. Shepard, J. A. Bhatti, and T. E. Humphreys, “Unmanned aircraft capture and control via GPS spooﬁng,” Journal of Field Robotics, vol. 31, no. 4, pp. 617–636, 2014

work page 2014

[13] [13]

Playing games for security: An efﬁcient exact algorithm for solving Bayesian Stackelberg games,

P. Paruchuri, J. P. Pearce, J. Marecki, M. Tambe, F. Ordonez, and S. Kraus, “Playing games for security: An efﬁcient exact algorithm for solving Bayesian Stackelberg games,” in Proc. of the Intl. Conf. on Autonomous agents and multiagent systems . International Foundation for Autonomous Agents and Multiagent Systems, 2008, pp. 895–902

work page 2008

[14] [14]

Stackelberg-game analysis of correlated attacks in cyber-physical systems,

M. Zhu and S. Martinez, “Stackelberg-game analysis of correlated attacks in cyber-physical systems,” in the Proc. of American Control Conf. IEEE, 2011, pp. 4063–4068

work page 2011

[15] [15]

Patrolling security games: Deﬁnition and algorithms for solving large instances with single patroller and single intruder,

N. Basilico, N. Gatti, and F. Amigoni, “Patrolling security games: Deﬁnition and algorithms for solving large instances with single patroller and single intruder,” Artiﬁcial Intelligence, vol. 184, pp. 78–123, 2012

work page 2012

[16] [16]

Tambe, Security and Game Theory: Algorithms, Deployed Systems, Lessons Learned

M. Tambe, Security and Game Theory: Algorithms, Deployed Systems, Lessons Learned. Cambridge University Press, 2011

work page 2011

[17] [17]

Prism-games: A model checker for stochastic multi-player games

T. Chen, V . Forejt, M. Z. Kwiatkowska, D. Parker, and A. Simaitis, “Prism-games: A model checker for stochastic multi-player games.” in the Proc. of Intl. Conf. on TACAS . Springer, 2013, pp. 185–191

work page 2013

[18] [18]

A stochastic games framework for veriﬁcation and control of discrete time stochastic hybrid systems,

J. Ding, M. Kamgarpour, S. Summers, A. Abate, J. Lygeros, and C. Tomlin, “A stochastic games framework for veriﬁcation and control of discrete time stochastic hybrid systems,” Automatica, vol. 49, no. 9, pp. 2665–2674, 2013

work page 2013

[19] [19]

Where’s Waldo? sensor-based temporal logic motion planning,

H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas, “Where’s Waldo? sensor-based temporal logic motion planning,” in the Proc. of IEEE Intl. Conf. on Robotics and Automation , 2007, pp. 3116–3121

work page 2007

[20] [20]

Sampling-based motion planning with temporal goals,

A. Bhatia, L. E. Kavraki, and M. Y . Vardi, “Sampling-based motion planning with temporal goals,” in the Proc. of IEEE Intl. Conf. on Robotics and Automation , 2010, pp. 2689–2696

work page 2010

[21] [21]

Motion planning with dynamics by a synergistic combination of layers of planning,

E. Plaku, L. E. Kavraki, and M. Y . Vardi, “Motion planning with dynamics by a synergistic combination of layers of planning,” IEEE Transactions on Robotics , vol. 26, no. 3, pp. 469–482, 2010

work page 2010

[22] [22]

Optimal temporal logic planning in probabilistic semantic maps,

J. Fu, N. Atanasov, U. Topcu, and G. J. Pappas, “Optimal temporal logic planning in probabilistic semantic maps,” in the Proc. of IEEE Intl. Conf. on Robotics and Automation , 2016, pp. 3690–3697

work page 2016

[23] [23]

Motion planning and control from temporal logic speciﬁcations with probabilis- tic satisfaction guarantees,

M. Lahijanian, J. Wasniewski, S. B. Andersson, and C. Belta, “Motion planning and control from temporal logic speciﬁcations with probabilis- tic satisfaction guarantees,” in the Proc. of IEEE Intl. Conf. on Robotics and Automation, 2010, pp. 3227–3232

work page 2010

[24] [24]

A fully automated framework for control of linear systems from temporal logic speciﬁcations,

M. Kloetzer and C. Belta, “A fully automated framework for control of linear systems from temporal logic speciﬁcations,” IEEE Transactions on Automatic Control , vol. 53, no. 1, pp. 287–297, 2008

work page 2008

[25] [25]

Synthesis of shared autonomy policies with tem- poral logic speciﬁcations,

J. Fu and U. Topcu, “Synthesis of shared autonomy policies with tem- poral logic speciﬁcations,” IEEE Transactions on Automation Science and Engineering, vol. 13, no. 1, pp. 7–17, 2016

work page 2016

[26] [26]

Analyzing unsynthesizable speciﬁcations for high-level robot behavior using LTLMoP,

V . Raman and H. Kress-Gazit, “Analyzing unsynthesizable speciﬁcations for high-level robot behavior using LTLMoP,” in Computer Aided Veriﬁcation. Springer, 2011, pp. 663–668

work page 2011

[27] [27]

Minimum-violation LTL planning with conﬂicting speciﬁcations,

J. Tumov ´a, L. I. R. Castro, S. Karaman, E. Frazzoli, and D. Rus, “Minimum-violation LTL planning with conﬂicting speciﬁcations,” in the Proc. of American Control Conf. IEEE, 2013, pp. 200–205

work page 2013

[28] [28]

Robust control of Markov decision pro- cesses with uncertain transition matrices,

A. Nilim and L. El Ghaoui, “Robust control of Markov decision pro- cesses with uncertain transition matrices,” Operations Research, vol. 53, no. 5, pp. 780–798, 2005

work page 2005

[29] [29]

Synthesis of joint control and active sensing strategies under temporal logic constraints,

J. Fu and U. Topcu, “Synthesis of joint control and active sensing strategies under temporal logic constraints,” IEEE Transactions on Automatic Control, vol. 61, no. 11, pp. 3464–3476, 2016

work page 2016

[30] [30]

Fudenberg and J

D. Fudenberg and J. Tirole, Game Theory. MIT Press, 1991

work page 1991

[31] [31]

Parameter synthesis for Markov models: Faster than ever,

T. Quatmann, C. Dehnert, N. Jansen, S. Junges, and J.-P. Katoen, “Parameter synthesis for Markov models: Faster than ever,” inIntl. Symp. on Automated Technology for Veriﬁcation and Analysis. Springer, 2016, pp. 50–67

work page 2016

[32] [32]

A game- based abstraction-reﬁnement framework for Markov decision processes,

M. Kattenbelt, M. Kwiatkowska, G. Norman, and D. Parker, “A game- based abstraction-reﬁnement framework for Markov decision processes,” Formal Methods in System Design , vol. 36, no. 3, pp. 246–280, 2010

work page 2010

[33] [33]

Concurrent omega-regular games,

L. de Alfaro and T. A. Henzinger, “Concurrent omega-regular games,” in Proc. of IEEE symp. on Logic in Computer Science , 2000, pp. 141–154

work page 2000

[34] [34]

A game theoretic study of attack and defense in cyber-physical systems,

C. Y . Ma, N. S. Rao, and D. K. Yau, “A game theoretic study of attack and defense in cyber-physical systems,” in the Proc. of IEEE Conf. on Computer Communications Workshops, 2011, pp. 708–713

work page 2011

[35] [35]

Jamming attacks on remote state estimation in cyber-physical systems: A game-theoretic approach,

Y . Li, L. Shi, P. Cheng, J. Chen, and D. E. Quevedo, “Jamming attacks on remote state estimation in cyber-physical systems: A game-theoretic approach,” IEEE Transactions on Automatic Control , vol. 60, no. 10, pp. 2831–2836, 2015

work page 2015

[36] [36]

Stackelberg vs. Nash in security games: An extended investigation of interchangeability, equivalence, and uniqueness,

D. Korzhyk, Z. Yin, C. Kiekintveld, V . Conitzer, and M. Tambe, “Stackelberg vs. Nash in security games: An extended investigation of interchangeability, equivalence, and uniqueness,” Journal of Artiﬁcial Intelligence Research, vol. 41, no. 2, pp. 297–327, 2011

work page 2011

[37] [37]

Secure control under linear temporal logic constraints

L. Niu and A. Clark, “Secure control under linear temporal logic constraints.” in the Proc. of American Control Conf. IEEE, 2018

work page 2018

[38] [38]

Event-triggered state observers for sparse sensor noise/attacks,

Y . Shoukry and P. Tabuada, “Event-triggered state observers for sparse sensor noise/attacks,” IEEE Transactions on Automatic Control, vol. 61, no. 8, pp. 2079–2091, 2016

work page 2079

[39] [39]

Secure estimation and control for cyber-physical systems under adversarial attacks,

H. Fawzi, P. Tabuada, and S. Diggavi, “Secure estimation and control for cyber-physical systems under adversarial attacks,” IEEE Transactions on Automatic Control, vol. 59, no. 6, pp. 1454–1467, 2014

work page 2014

[40] [40]

Game theory meets network security and privacy,

M. H. Manshaei, Q. Zhu, T. Alpcan, T. Bacs ¸ar, and J.-P. Hubaux, “Game theory meets network security and privacy,” ACM Computing Surveys , vol. 45, no. 3, p. 25, 2013

work page 2013

[41] [41]

Game-theoretic methods for robustness, security, and resilience of cyberphysical control systems: games-in-games prin- ciple for optimal cross-layer resilient control systems,

Q. Zhu and T. Basar, “Game-theoretic methods for robustness, security, and resilience of cyberphysical control systems: games-in-games prin- ciple for optimal cross-layer resilient control systems,” IEEE Control Systems Magazine, vol. 35, no. 1, pp. 46–65, 2015

work page 2015

[42] [42]

Robust and resilient control design for cyber- physical systems with an application to power systems,

Q. Zhu and T. Bas ¸ar, “Robust and resilient control design for cyber- physical systems with an application to power systems,” in the Proc. of the 50th IEEE Conf. on Decision and Control and European Control Conf., 2011, pp. 4066–4071

work page 2011

[43] [43]

D. P. Bertsekas, D. P. Bertsekas, D. P. Bertsekas, and D. P. Bertsekas, Dynamic Programming and Optimal Control . Athena Scientiﬁc Bel- mont, MA, 1995, vol. 1, no. 2

work page 1995

[44] [44]

A probabilistic approach for control of a stochastic system from LTL speciﬁcations,

M. Lahijanian, S. B. Andersson, and C. Belta, “A probabilistic approach for control of a stochastic system from LTL speciﬁcations,” in the Proc. of the 48th IEEE Conf. on Decision and Control/Chinese Control Conf. , 2009, pp. 2236–2241

work page 2009

[45] [45]

An overview of existing methods and recent advances in sequential monte carlo,

O. Capp ´e, S. J. Godsill, and E. Moulines, “An overview of existing methods and recent advances in sequential monte carlo,” Proceedings of the IEEE , vol. 95, no. 5, pp. 899–924, 2007

work page 2007

[46] [46]

Zur theorie der gesellschaftsspiele,

J. v. Neumann, “Zur theorie der gesellschaftsspiele,” Mathematische annalen, vol. 100, no. 1, pp. 295–320, 1928

work page 1928

[47] [47]

Hogben, Handbook of Linear Algebra

L. Hogben, Handbook of Linear Algebra . Chapman and Hall/CRC, 2013. Luyao Niu (SM’15) received the B.Eng. degree from the School of Electro-Mechanical Engineering, Xidian University, Xian, China, in 2013 and the M.Sc. degree from the Department of Electrical and Computer Engineering, Worcester Polytechnic Insti- tute (WPI) in 2015. He has been working tow...

work page 2013