Titlebook: Reachability Problems; 10th International W Kim Guldstrand Larsen,Igor Potapov,Jiří Srba Conference proceedings 2016 Springer International

同义联想法

Safety Property-Driven Stubborn Sets,the safety property that is being verified. Typical earlier methods only take the property into account in one state of each cycle or in one state of each terminal strong component of the reduced state space. They may fire totally irrelevant transitions in the other states. Where the property is tak

隼鹰

Characterizing Word Problems of Groups,s of the group that represent the identity element of the group. This definition allows us to consider a word problem as a formal language and a rich topic of research concerns the connection between the complexity of this language and the algebraic structure of the corresponding group..Another inte

archenemy

Distributed Synthesis of State-Dependent Switching Control,the state space, the method builds a capture set . and a control which steers any element of . into .. The method works by iterated backward reachability from .. More precisely, . is given as a parametric extension of ., and the maximum value of the parameter is solved by linear programming. The met

deactivate

Compositional Analysis of Boolean Networks Using Local Fixed-Point Iterations,olean network (BN). This merely consists in replacing a global fixed-point computation by a composition of local fixed-point computations. Once these approximations have been computed, it becomes much more tractable to generate the exact sets of attractors and basins of attraction. We illustrate the

澄清

Decidable Models of Integer-Manipulating Programs with Recursive Parallelism, integer variables. Since the threads in each program configuration are structured in a hierarchical fashion, our model is state-extended ground-tree rewrite systems equipped with shared unbounded integer counters that can be incremented, decremented, and compared against an integer constant. Since