• Không có kết quả nào được tìm thấy

Computer Aided Verification

N/A
N/A
Nguyễn Gia Hào

Academic year: 2023

Chia sẻ "Computer Aided Verification"

Copied!
238
0
0

Loading.... (view fulltext now)

Văn bản

The error table can be used offline to debug (explain) the generated counter-examples or online to direct the sampler to certain regions of the abstract feature space. The neural network misclassifies the traffic cones due to the orange vehicle in the background, leading to an accident.

Fig. 1. Structure and operation of V ERIF AI.
Fig. 1. Structure and operation of V ERIF AI.

1 Introduction

The network is evaluated by assigning values ​​to the neurons in the input layer, and then using these values ​​to iteratively calculate the neuron assignments in each subsequent layer. A neuron's assignment is determined by computing a weighted sum of neuron assignments from the previous layer, and then applying to the result a nonlinear activation function, such as the Corrected Linear Unit (ReLU) function, ReLU(x) = max (0, x).

2 Design of Marabou

  • Simplex Core ( Tableau and BasisFactorization Classes)
  • Piecewise-Linear Constraints (PiecewiseLinearConstraint Class)
  • The Engine (Engine and SmtCore Classes)
  • Input Interfaces (AcasParser class, maraboupy Folder)

Constraint-level constraint tightening is performed by querying the piecewise-linear constraints for tighter constraints using the getEntailedTightenings() method. The engine stores and coordinates the various solution components, including the simplex kernel and the piecewise linear constraints.

3 Evaluation

Figure 2 shows the average runtime of Marabou and ReluVal on the ACAS Xu properties, as a function of the number of available cores. We see that as the number of cores increases, Marabou (solid) is able to close the gap and sometimes outperform ReluVal (dotted).

4 Conclusion

Silver, D., et al.: Motion game learning with deep neural networks and search trees. Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals.

Systems

Our framework requires the encoding of the systems and the proofs in the first-order theory of the universal automaton structure. To the best of our knowledge, our method is the first automatic technique that proves the anonymity property of the protocols in the parameterized case.

2 Preliminaries

It is standard (e.g. see [34]) to impose the minimal probability assumption on the PTS we will be dealing with, i.e. there is > 0 such that any transition with a non-zero probability satisfies >. The minimal probability assumption implies, among other things, that the PTS is bounded-branching (i.e. that its underlying transition graph is bounded-branching).

3 Framework of Regular Relations

The decidability of the first-order theory of U follows using a standard auto-theoretical algorithm (see e.g. [9,49]). In the following, we will also use the term regular relations to denote relations defined in U.

4 Probabilistic Bisimilarity Within Regular Relations

Specifying a Probabilistic Transition System

Therefore, we can now assume that the transition probability functions have the interval N. The challenge now is that our encoding of a PTS in the universal automatic structure must encode two different types of words over a finite alphabet Σ: configurations and natural weights. The graph of the transition probability function can be described by a first-order formula ϕ(x, y, z) :=ϕloop(x, y, z)∨ϕmove(x, y, z) over U, where.

Proof Rules for Probabilistic Bisimulation

A PTS configuration is a word in QΓ∗ consisting of a state in Q and a word above the stack symbols. A transition can be used if the configuration prefix matches the left side of the above transition rules.

Proof of Theorem 1

The first two requirements are easy to express as a first order formula and are therefore algorithmic over U. 1≤i≤Nδa(x, yi, zi)∧ . 1≤i≤Nzi=wa), which is a first order formula and is algorithmic over U by the fact that the addition of a fixed number of weights is regular (as shown earlier in this section).

5 Application to Anonymity Verification

The grades protocol [29] is a multi-party computational algorithm that aims to safely calculate the sum of the participants' secrets. The anonymity feature of the protocol states that no participant can deduce the secrets of the other participants from the information she has observed.

6 Learning Probabilistic Bisimulations

In: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, pp. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, 13–167, Junie 13–167.

Analysis of Chemical Reaction Networks

An algorithm to abstract CRNs into semi-quantitative models based on interval abstraction of the species population and on transition acceleration. The LNA approach and an adaptive partitioning of the species according to jump conditions (it is more general than partitioning based on population thresholds) were proposed in [9].

2 Chemical Reaction Networks

Note that SSA produces a single realization of the stochastic process, whereas the stochastic solution of CME gives the probability distribution of each species over time. The behavior of the stochastic system X(t) can be described by the (possibly infinite) continuous Markov chain (CTMC) γ(N) = (S,X0,R), where the transition matrix R(i,j) gives the probability of a transition fromXi toXj.

3 Semi-quantitative Abstraction

The goals of the action in the abstract setting are abstractions of all possible concrete successors, i.e. The abstract rate is the smallest interval including all concrete rates of the respective concrete transitions.

Fig. 1. Above: Interval CTMDP abstraction with intervals on rates and non- non-determinism
Fig. 1. Above: Interval CTMDP abstraction with intervals on rates and non- non-determinism

Operational Semantics: Concretisation to a Representative The next disadvantage of classical abstraction philosophy, manifested in the

Note that this decision becomes more precise not only as we refine the population levels, but also as the system becomes more rigid (the specific values ​​of the levels vary more), which are usually more difficult to analyze. For ease of representation in our case studies, we will only show the size of the rates, ie.

4 Semi-quantitative Analysis

Further, t may be in the transient part leading to C, in which case these states are added to C and the steady state changes slightly, spreading the distribution a little to the earlier transient states as well. In fact, it corresponds to the steady-state distribution if BSCC is a cycle and minStayingRate is significantly larger than other rates in BSCC, since the return time of the states is approx. m/minStayingRate and the staying time 1/stayingRate(·).

5 Experimental Evaluation and Discussion

  • Gene Expression Model
  • Goutsias’s Model
  • Viral Infection
  • Stochastic Games
  • Reachability Objective
  • Bounded and Asynchronous Value Iteration
  • INITIALIZE BOUNDS 3: repeat

The concrete quantities (i.e. the extinction probability and the mean RNA population) are closer to the analysis in [43]. Munsky, B., Khammash, M.: The finite state projection algorithm for solving the chemical master equation.

Table 1. Gene expression. For slow DNA switching, r 1 = r 2 = 0 . 05. For fast DNA switching, r 1 = r 2 = 1
Table 1. Gene expression. For slow DNA switching, r 1 = r 2 = 0 . 05. For fast DNA switching, r 1 = r 2 = 1

3 Algorithm

  • Model-Based
  • Safe Updates with Confidence Intervals Using Distributed Error Probability
  • Improved EC Detection
  • Adapting to Games: Deflating MSECs
  • Guidance and Statistical Guarantee
  • Utilizing the Additional Information of Grey Box Input

Choice of δk: For each of the full BVI phases, we construct a submodel that is correct with probability (1−δk). Note that the precision is independent of the input parameter ε and can always be 1 in the worst case.

Fig. 1. A running example of an SG. The dashed part is only relevant for the later examples
Fig. 1. A running example of an SG. The dashed part is only relevant for the later examples

4 Experimental Evaluation

For the boundaries, note that the equations for Earth U both have two parts: the usual Bellman part and the residual probability multiplied by the more conservative boundary assumption, i.e. Figure 2 shows the evolution of the lower and upper bounds in the gray and black box settings for 4 different models.

Table 1. Achieved precision ε  given by our algorithm in both grey and black box settings after running for a period of 30 min (See the paragraph below Theorem 1 for why we use ε  and not ε)
Table 1. Achieved precision ε given by our algorithm in both grey and black box settings after running for a period of 30 min (See the paragraph below Theorem 1 for why we use ε and not ε)

5 Conclusion

BFHH11] Bogdoll, J., Ferrer Fioriti, L.M., Hartmanns, A., Hermanns, H.: Partial-order methods for statistical model verification and simulation. DHKP16] Daca, P., Henzinger, T.A., Kˇret´ınsk´y, J., Petrov, T.: Faster statistical model checking for unconstrained temporal properties.

Specifications Parametric in Time and Data

In addition, we show that we can detect log segments (start and end dates) for which a specification exists. We believe that our framework balances expressiveness and monitoring performance well: (i) Regarding expressiveness, the comparison with existing work is summarized in Table 1 (see Section 2 for further details). ii) Our monitor is complete, in the sense that it returns a symbolic constraint that characterizes all parameter estimates that match a given specification. (iii) We also achieve.

Table 1. Comparison of monitoring expressiveness
Table 1. Comparison of monitoring expressiveness

2 Related Works

The output comes in the form of a subset of the parameter space for which the formula on the log applies. On the other hand, a series of works consider temporal words, with specifications in the form of temporal automata [4,36].

3 Preliminaries

That is, [μ]η(ζ(PDU)) computes a new (non-parametric) evaluation of the variable obtained after applying to μ the partial PDU function evaluated by ζ. Let μ be the evaluation of the variable such that μ(v1) = 1 and μ(v2) = 2, and let η be the evaluation of the local variable such that η(lv1) = 2 and η(lv2) is undefined.

Table 2. Variables, parameters and valuations used in guards
Table 2. Variables, parameters and valuations used in guards

4 Parametric Timed Data Automata

Consider the data type for rationals, the variables set{v1, v2}, the local variables set{lv1,lv2}and the parameters set{vp1}. The domain conditions ondg andPDUVensure that the local variables used in the wait (resp. update) are only those in the action signature Dom(a).

5 Symbolic Monitoring Against PTDA Specifications

Problem Definition

Online Algorithm

For the rational number data type in Example 2, variables and data parameter values ​​Vd can be represented by convex polyhedra and the above operations terminate. For the data type for stringsS in Example 2, variable and data parameter values ​​Vd can be represented by S|V|×(S∪ Pfin(S))|VP|and the above operations terminate, where Pfin(S) is the set of finite sets of S.

Encoding Parametric Timed Pattern Matching

For variable valuations and data parameter valuations we need an appropriate representation depending on the data type (D,DE,DU). For any PTDA A over a data type (D,DE,DU) and actionsΣε, and for any temporal data wordwoverΣ, Algorithm1 terminates if the following operations terminate on the symbolic representation Vd of a set of variable and data parameter valuations.

6 Experiments

Benchmark 1: Copy

The automaton can non-deterministically stay in 0 or start measuring the log so that the ε-transition to1 checks c=tp1 and therefore “remembers” the starting time using the time parameter tp1. Then, every time user vp withdraws more than half of the accumulated withdrawals (data protection 2v1 > v2) in the (50,100) time window (time protection c−tp, the automaton performs an ε-transition to the receiving location, checks c = tp2 and therefore remembers the final time using the time parameter tp2.

Benchmark 2: Dominant

The string n represents the username and the integer represents the withdrawal amount by user n. Actions are Σ={withdraw} and Dom(withdraw) ={a} while has an integer value representing the withdrawal amount.

Fig. 4. Execution time (left) and memory usage (right) of Copy
Fig. 4. Execution time (left) and memory usage (right) of Copy

Discussion

We notice that the execution time is linear with the number of events and the memory usage is more or less constant with respect to the number of events.

7 Conclusion and Perspectives

Brim, L., Dluhos, P., Safr´anek, D., Vejpustek, T.: STL∗: extending signal temporal logic with the signal value freeze operator. Images or other third-party material in this chapter are covered under the chapter's Creative Commons license, unless otherwise indicated in a credit line for the material.

Model-Checker for INfinite-State Analysis

The error probability calculated during the model checking depends on the depth of state exploration. The calculated probability forms a lower bound on the probability, while the upper bound also includes the probability of the absorbing state.

2 STAMINA

State Space Approximation

It starts from the initial state whose reachability value, i.e., ˆκ(x0), is initialized to 1.0 as shown in Figure 2a. The reachability value inx0 is distributed to its successor states based on the probability of outgoing transitions from x0 to its successor state.

Figure 2 illustrates the standard breadth first search (BFS) state exploration for reachability threshold κ = 0.25
Figure 2 illustrates the standard breadth first search (BFS) state exploration for reachability threshold κ = 0.25

Property Based State Space Exploration

3 Results

The later experiments initialize IPTG to 0 to calculate the failure rate, that is, the probability that the circuit erroneously changes state within a cell cycle of 2,100s (an approximation of the cell cycle in E. coli [24]). This paper considers the probability that the first queue becomes full in 0.25 time units, represented by the CSL property P=?[trueU0.25queue1 vol].

Table 1. Verification results for genetic toggle switch.
Table 1. Verification results for genetic toggle switch.

4 Conclusions

Motivating Example

The abstract high-level specification, AEPS, of an event processing system is defined as follows. The next event is scheduled to occur at time t=k; so it is updated in one step.

Fig. 1. Event simulation system
Fig. 1. Event simulation system

3 Theory of Skipping Refinement

Algebraic Properties

We define a function,r, that given, corresponding to the index of a partition of τ under β, returns the index of the partition of τ under θ, in which the first element of τ'sithpartition under β is located.r.i=j iffθ.j≤β.i < θ(j+ 1). Given , corresponding to the index of a division of σunderπ, the function returns the index of the corresponding division of σunderα.

Skipping Refinement

Under a refinement map, soap, which extracts the set of event-time pairs in the priority order of MPEPS, a step in MPEPS can correspond to a step in MEPS. Next, we account for the difference between MEPS and AEPS in the number of events that the two systems can perform in a single step.

4 Mechanised Reasoning

Next, we define locally well-founded skipping simulation (LWFSK), a skipping simulation characterization that separates skipping and stuttering inference on the right (Figure 2). Local well-grounded hopping simulation (orange line indicates band-coupled states and blue line indicates O-coupled states) (Color figure online).

Fig. 2. Local well-founded skipping simulation (orange line indicates the states are related by B and blue line indicate the states are related by O ) (Color figure online)
Fig. 2. Local well-founded skipping simulation (orange line indicates the states are related by B and blue line indicate the states are related by O ) (Color figure online)

5 Case Study (Event Processing System)

Third, we have a collection of lemmas that show that inserting and removing two equivalent sets of timed events from a scheduler results in an equivalent scheduler. And fourth, we have a collection of lemmas that show that two schedulers are equivalent if they are set equal.

6 Related Work

First, we have a collection of lemmas to prove the functions' input-output contracts. Second, we have a collection of lemmas to show that operations on the schedulers in the three systems preserve different invariants, e.g. that any timed event in the scheduler is scheduled to run at a time greater than or equal to the current time.

7 Conclusion and Future Work

The full verification of CertiKOS [6,7], an OS kernel, is based on the notion of simulation refinement. If the material is not covered by the chapter's Creative Commons license and your intended use is not permitted by legal regulations or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

B¨ uchi Automata: A Symbolic Approach

In the context of robustness, this strategy should be tolerant of small perturbations of the delays. Our algorithm can be understood as an adaptation to the robustness setting of the standard algorithm for B¨uchi acceptance in timed automata [17].

2 Timed Automata: Reachability and Robustness

A strategy for the controller is a functionσCon that maps every non-maximal game ending in some (, ν)∈SC to a pair (d, e) where >0 ande∈E such that there is a transition from (, ν) to (, ν, d, e). The parameterized robust controller synthesis problem asks, given a timed automaton A, whether there existsδ >0 such that the controller has a winning strategy in Gδ(A).

3 Reachability Relation of a Path

In other words, in the constraint graph, this constraint is the minimum weight between the sum of the weights of the edges (Xdr, Xal) and (Xbl, Xcr) and the sum of the weights of the edges (Xbl, Xal) and (Xdr, Xcr). Then the normalization of the graph describes the reachability relation along the path ending in zoneZ.

4 Robust Iterability of a Lasso

Given a path ρ, one can compute a contracted DBM (M, P) equal to the largest fixed point of the CPreδr operator. One first computes a symbolic representation, valid for all values ​​of δ, of the largest fixation point of CPreδr2.

Fig. 2. On the left, the branching constraint graph G δ e 1 e 2 encoding the operator CPre δ e 1 e 2 , where e 1 and e 2 refer to edges considered in Fig
Fig. 2. On the left, the branching constraint graph G δ e 1 e 2 encoding the operator CPre δ e 1 e 2 , where e 1 and e 2 refer to edges considered in Fig

5 Synthesis of Robust Controllers

The correction of this uptake check is given in the following lemma, where Reachnpρ denotes the reachability relation associated with ρ in the automaton Anp. Indeed, we can prove that the non-punctual reachability relation we consider reflects the existence of non-punctual aperiodic paths in the region automaton, as considered in [25].

6 Case Study

Therefore, to test the robustness of lasaρ1ρ2, it is sufficient to store only the string Postnpρ1(0) and. Inaccurate advance analysis. As a consequence of the previous theorem, we can use the classical forward analysis of the time automaton Anp to find the prefixρ1 lassoρ1ρ2.

Fig. 4. Summary of experiments with different sizes. In each scenario, we assign a different objective to a subset of trains
Fig. 4. Summary of experiments with different sizes. In each scenario, we assign a different objective to a subset of trains

7 Conclusion

  • Bottlenecks in Abstraction-Based Control Synthesis
  • Methodology
  • Contributions
  • Notation

To our knowledge, the application of relational interfaces to robust abstraction-based control synthesis is new. The second half applies those insights to the finite abstraction approach to control synthesis.

Fig. 1. By expressing many different techniques within a common framework, users are able to rapidly develop methods to exploit system structure in controller synthesis.
Fig. 1. By expressing many different techniques within a common framework, users are able to rapidly develop methods to exploit system structure in controller synthesis.

2 Control Synthesis for a Motivating Example

As an example if it is associated with an M-dimensional Euclidean spaceRM, then it is a composite variable that can be broken apart into a collection of atomic variables v1,. Approximate solution to the Dubins vehicle reaching game visualized as a subset of the state space.

3 Relational Interfaces

Atomic and Composite Operators

Any acyclic interconnection can be composed into a single interface by systematically applying Definition 4's binary composition operator. In contrast to the composition and output hide operators, this operator is not included in the standard theory of relational interfaces [22] and was added to encode a controller antecedent which was subsequently used in Eq.

Constructing Control Synthesis Pipelines

Arraying interfaces has a built-in notion of robustness to account for the non-deterministic outputs of F1 and the blocking of inputs to F2 via the shared variables io12. If the sink is seen as a constraint, an input variable is "hidden" by an angelic environment that chooses an input assignment to satisfy the constraint.

Modifying the Control Synthesis Pipeline

4 Interface Abstraction via Quantization

Theory of Abstract Interfaces

Second, if both systems accept input, the abstract output set is a superset of the concrete function's output set. An abstract interface is a conservative representation of a concrete interface because the abstraction accepts fewer inputs and exposes more non-deterministic outputs.

Fig. 4. Example depiction of the refinement partial order. Each small plot on the depicts input-output pairs that satisfy an interface’s predicate
Fig. 4. Example depiction of the refinement partial order. Each small plot on the depicts input-output pairs that satisfy an interface’s predicate

Dynamically Coarsening Interfaces

This reward function can be used in practice because augmentation is computationally cheaper than composition. For BDDs, the winning region can be coarsened until the number of nodes reduces below a desired threshold.

Fig. 6. Number of BDD nodes (red) and number of states in reach basin (blue) with respect to the reach game iteration with a greedy quantization
Fig. 6. Number of BDD nodes (red) and number of states in reach basin (blue) with respect to the reach game iteration with a greedy quantization

5 Refining System Dynamics

Constructing Finite Interfaces Through Shared Refinement A common method to construct finite abstractions is through simulation and

Smaller interfaces are constructed by sampling regions of the input space and constructing an input-output pair. An individual sampled abstraction is not useful for synthesis because it is limited to a local part of the interface input space.

Fig. 7. (Left) Result of sample and coarsen operations for control system interface F ( x ∪ u, x + )
Fig. 7. (Left) Result of sample and coarsen operations for control system interface F ( x ∪ u, x + )

6 Decomposed Control Predecessor

I: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (Part of CPS Week), HSCC 2018, pp. I: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017, pp.

Fig. 9. A monolithic cpre ( · ) incurs unnecessary pre-processing and synthesis runtime costs for the Dubins vehicle reach game
Fig. 9. A monolithic cpre ( · ) incurs unnecessary pre-processing and synthesis runtime costs for the Dubins vehicle reach game

Synthesis Beyond the Bools

On the other hand, this quantification is also the reason why the synthesis problem cannot be decided. This approach undermines the actual TSL synthesis problem by leaving the interpretation of the predicates to the environment.

Fig. 1. The TSL synthesis procedure uses a modular design. Each step takes input from the previous step as well as interchangeable modules (dashed boxes).
Fig. 1. The TSL synthesis procedure uses a modular design. Each step takes input from the previous step as well as interchangeable modules (dashed boxes).

2 Motivating Example

The first time the user exits the app while music is playing, the music pauses. In a handwritten program, this new functionality requires an additional wasPlaying variable to track the state of the music.

Fig. 3. The effect of a minor change in functionality on code versus a specification.
Fig. 3. The effect of a minor change in functionality on code versus a specification.

4 Temporal Stream Logic

An n-ary function f:Vn → V determines new values ​​from given values, where the set of all functions (of arbitrary arity) is given by F. AΦ-labeled andΥ-branched tree is a functionσ:Υ∗→Φ, whereΥ denotes the set of branching directions along a tree.

Fig. 4. General architecture of reactive systems that are specified in TSL on the left, and the structure of function, predicate and updates on the right.
Fig. 4. General architecture of reactive systems that are specified in TSL on the left, and the structure of function, predicate and updates on the right.

5 TSL Properties

We may not have added enough environmental assumptions to the approximation for the system to arrive at a realization strategy. Due to the definition of realizability, the environment may choose function and predicate assignments differently for each system strategy.

Fig. 5. A TSL specification (a) with input x and cell y that is realizable. A winning strategy is to save x to y as soon as p ( x ) is satisfied
Fig. 5. A TSL specification (a) with input x and cell y that is realizable. A winning strategy is to save x to y as soon as p ( x ) is satisfied

6 TSL Synthesis

Control flow model. The first step of our approach is the synthesis of the control flow model M(CFM) from the given specification TSL ϕ, which provides us with a unified representation of the control flow structure of our final program. Using the powerful CCA core, we can even directly implement the player in hardware, which is for example possible with the CλaSH compiler [3].

Fig. 6. Example CFM of the music player generated from a TSL specification.
Fig. 6. Example CFM of the music player generated from a TSL specification.

7 Experimental Results

In the final step, the synthesized FRP program is compiled into an executable, using the given function and predicate implementations. Number of cells|CM|and vertices|VM|of the resulting CFMM and synthesis times for a collection of TSLϕ specifications.

Table 1. Number of cells |C M | and vertices |V M | of the resulting CFM M and syn- syn-thesis times for a collection of TSL specifications ϕ
Table 1. Number of cells |C M | and vertices |V M | of the resulting CFM M and syn- syn-thesis times for a collection of TSL specifications ϕ

8 Related Work

We also considered a preliminary set of benchmarks that require multiple refinement steps to be synthesized. In doing so, the system needs purity not only to verify this condition, but also to make the right decisions in the resulting implementation to be synthesized.

9 Conclusions

Jeffrey, A.: LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs. ed.). Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1–3, 2015, pp.

Through Quantitative Games

Related Work

As mentioned earlier, a challenge with quantitative specifications is that, unlike safety specifications, a non-interference usually does not have a devastating effect, so it is not trivial to decide when and to what extent to intervene. However, the settings are very different, since the forced program is not reactive, while we assume a plant that receives commands.

2 Definitions and Problem Statement

Plants, Controllers, and Shields

Hình ảnh

Fig. 2. A scalability comparison of Marabou and ReluVal on ACAS Xu.
Figure 2 shows the average runtime of Marabou and ReluVal on the ACAS Xu  prop-erties, as a function of the number of  avail-able cores
Fig. 1. Above: Interval CTMDP abstraction with intervals on rates and non- non-determinism
Table 1. Gene expression. For slow DNA switching, r 1 = r 2 = 0 . 05. For fast DNA switching, r 1 = r 2 = 1
+7

Tài liệu tham khảo

Tài liệu liên quan