검색 상세

Model Checking of Signal Temporal Logic : Robust model checking of signal temporal logic for hybrid systems

  • 이지아 (Jia Lee, 포항공과대학교 일반대학원)

초록/요약

Signal temporal logic (STL) is a temporal logic formalism used to specify properties of continuous signals. STL has been widely applied in specifying, monitoring, and testing properties of hybrid systems that exhibit both discrete and continuous behavior. However, model checking techniques for hybrid systems have primarily been limited to invariant and reachability properties. This thesis introduces model checking algorithms and a tool for general STL properties of hybrid systems. To overcome the limitations of existing techniques, we developed an efficient algorithm that reduces the encoding size of the STL bounded model checking problem. We demonstrate the effectiveness of our new technique on a number of hybrid system case studies. Second, we define robust STL bounded model checking problem that can flexibly handle small perturbations in the signals. We propose a technique to solve the robust STL bounded model checking problem by reducing the problem to Boolean STL model checking. Based on the the technique, we develop a model checker, called STLmc, for STL properties of hybrid systems. If STLmc finds no counterexample, the system is guaranteed to be correct within the given bounds and robustness threshold. Finally, we extend our approach to integrate with reachable-set computation technique. We propose an automata-based technique for the robust STL model checking problem. Given a hybrid system, an STL formula, and a robustness threshold, we build a hybrid automaton such that a counterexample signal of the formula exists in the hybrid system if a designated goal mode of the hybrid automaton is reachable. We also extend the automata-based technique to handle STL model checking problem over unbounded signals.

more

목차

I. Introduction 1
1.1 Logical Foundations 3
1.2 SMT-Based Robust STL Model Checking 4
1.3 Automata-Based Robust STL Model Checking 5
II. Background 8
2.1 Signal Temporal Logic 8
2.2 Variable Points 11
2.3 Hybrid Automata 14
2.4 Boolean STL Model Checking 15
2.5 Syntactic Separation 16
III. Logical Foundations 19
3.1 SMT-Based Bounded STL Model Checking 19
3.2 Partition Construction 21
3.2.1 Stability Conditions 21
3.2.2 Stable Refinements 23
3.2.3 Fully Stable Refinements for STL 27
3.3 Robust STL Model Checking 28
IV. SMT-Based Robust STL Bounded Model Checking 36
4.1 Encoding of STL and Hybrid Automata 36
4.1.1 Symbolic Representation of Discrete Signals 36
4.1.2 Encoding of Discrete Signals for STL 37
4.1.3 Encoding of Fully Stable Partitions 39
4.1.4 Encoding of Matching Trajectories in Hybrid Automata . 42
– III –
4.2 Bounded Robust STL Model Checking Algorithm 43
4.2.1 Two-Step Solving Algorithm 44
4.2.2 Handling Universal Quantification 46
4.3 Experimental Evaluation 51
4.3.1 STL Model Checking of Hybrid Automata 51
4.3.2 Bounded STL Satisfiability Checking 52
4.3.3 Comparison with Reachability Analysis Tools 54
V. Automata-Based Robust STL Model Checking 57
5.1 Robustly Stable Partitions 58
5.2 Interval Predicates and Decomposition Rules 61
5.2.1 Interval Predicates 61
5.2.2 Interval Sequence Judgements 64
5.2.3 Decomposition Rules 65
5.3 Constructing Hybrid Automata for STL 79
5.3.1 Transition Form and Closures 80
5.3.2 Constructing Tableau for STL 85
5.3.3 Finiteness of Tableau 89
5.3.4 Tableau Minimization 92
5.3.5 Transform Tableau into Hybrid Automata 95
5.4 Experimental Evaluation 98
5.4.1 STL Model Checking of Hybrid Automata 98
5.4.2 Tableau Construction for STL formulas 99
5.5 Verifying STL over Unbounded Signals 100
5.5.1 Tableau for Unbounded Signals Satisfying STL 100
5.5.2 Checking STL Tableau for Unbounded Signals 103
VI. Related Works 105
VII. Conclusions and Future Works 108
Summary (in Korean) 110
– IV –
References 112
Summary (in Korean) 125
– V –

more
반출 Meta View 목록