Wyniki wyszukiwania - BazTech

1

SMT-based reachability analysis for simply-timed systems

Zbrzezny A. M., Zbrzezny A.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

|

2015

|

Vol. 20

83--92

EN

In the paper we present Satisfiability Modulo Theory based (SMT-based) reachability analysis algorithm for Simply-Timed Systems (i.e., Kripke structures where each transition holds a duration, which is an arbitrary natural number) generated by simply-timed automata. The algorithm is based on a SMT-based encoding for Simply-Timed Systems. We have tested the algorithm in question by using the generic simply timed pipeline paradigm model as the benchmark. The performance evaluation of the algorithm is given by means of the running time and the memory used.

2

Improving Reachability Analysis of Infinite State Systems by Specialization

Fioravanti F., Pettorossi A., Proietti M., Senni V.

Fundamenta Informaticae

|

2012

|

Vol. 119, nr 3/4

281-300

EN

We consider infinite state reactive systems specified by using linear constraints over the integers, and we address the problem of verifying safety properties of these systems by applying reachability analysis techniques. We propose a method based on program specialization, which improves the effectiveness of the backward and forward reachability analyses. For backward reachability our method consists in: (i) specializing the reactive system with respect to the initial states, and then (ii) applying to the specialized system the reachability analysis that works backwards from the unsafe states. For reasons of efficiency, during specialization we make use of a relaxation from integers to reals. In particular, we test the satisfiability or entailment of constraints over the real numbers, while preserving the reachability properties of the reactive systems when constraints are interpreted over the integers. For forward reachability our method works as for backward reachability, except that the role of the initial states and the unsafe states are interchanged. We have implemented our method using the MAP transformation system and the ALV verification system. Through various experiments performed on several infinite state systems, we have shown that our specialization-based verification technique considerably increases the number of successful verifications without a significant degradation of the time performance.

3

Verification techniques for sensitivity analysis and design of controllers for nonlinear dynamic systems with uncertainties

Rauh A., Minisini J., Hofer E. P.

International Journal of Applied Mathematics and Computer Science

|

2009

|

Vol. 19, no 3

425-439

EN

Control strategies for nonlinear dynamical systems often make use of special system properties, which are, for example, differential flatness or exact input-output as well as input-to-state linearizability. However, approaches using these properties are unavoidably limited to specific classes of mathematical models. To generalize design procedures and to account for parameter uncertainties as well as modeling errors, an interval arithmetic approach for verified simulation of continuoustime dynamical system models is extended. These extensions are the synthesis, sensitivity analysis, and optimization of open-loop and closed-loop controllers. In addition to the calculation of guaranteed enclosures of the sets of all reachable states, interval arithmetic routines have been developed which verify the controllability and observability of the states of uncertain dynamic systems. Furthermore, they assure asymptotic stability of controlled systems for all possible operating conditions. Based on these results, techniques for trajectory planning can be developed which determine reference signals for linear and nonlinear controllers. For that purpose, limitations of the control variables are taken into account as further constraints. Due to the use of interval techniques, issues of the functionality, robustness, and safety of dynamic systems can be treated in a unified design approach. The presented algorithms are demonstrated for a nonlinear uncertain model of biological wastewater treatment plants.

4

Modelling and Simulation of Quantum Teleportation and Dense Coding Using Predicate/Transition-Nets

Varpaaniemi K., Ojala L.

Fundamenta Informaticae

|

2008

|

Vol. 85, nr 1-4

465-479

EN

Reachability analysis is one of the most successful methods used in design and validation of protocols for classical communication, whereas the predicate/transition-net formalism is one of the most appropriate formalisms for reachability analysis oriented modelling. Quantum teleportation and dense coding are non-classical communication protocols that have been widely researched in the field of quantum computing. In this article, we present predicate/transition-net models of these two protocols and use the PROD reachability analysis tool for analysing the models.

5

Narrowing Petri Net State Spaces Using the State Equation

Schmidt K.

Fundamenta Informaticae

|

2001

|

Vol. 47, nr 3,4

325-335

EN

Given a (possibly partially defined) state, all count vectors of transition sequences reaching that state are solutions to a corresponding Petri net state equation. We propose a search strategy where sequences corresponding to a minimal solution of the state equation are explored first. Then step by step the search space is relaxed to arbitrary count vectors. This heuristics relies on the observation that in many (though provably not in all) cases, minimal solutions of the state equation can be realized as a firing sequence. If no target state is reachable, either the state equation does not have solutions, or our search method would yield the full state space. We study the impact of the state equation on reachability, present an algorithm that exploits information from the state equation and discuss its application in stateless search as well as its combination with stubborn set reduction.

6

Stable models for stubborn sets

Varpaaniemi K.

Fundamenta Informaticae

|

2000

|

Vol. 43, Nr 1-4

355-375

EN

The stubborn set method is one of the methods that try to relieve the state space explosion problem that occurs in state space generation. Spending some time in looking for "good'" stubborn sets can pay off in the total time spent in generating a reduced state space. This article shows how the method can exploit tools that solve certain problems of logic programs. The restriction of a definition of stubbornness to a given state can be translated into a variable-free logic program. When a stubborn set satisfying additional constraints is wanted, the additional constraints should be translated, too. It is easy to make the translation in such a way that each acceptable stubborn set of the state is represented by at least one stable model of the program, each stable model of the program represents at least one acceptable stubborn set of the state, and for each pair in the representation relation, the number of certain atoms in the stable model is equal to the number of enabled transitions of the represented stubborn set. So, in order to find a stubborn set which is good w.r.t. the number of enabled transitions, it suffices to find a stable model which is good w.r.t. the number of certain atoms. The article also presents a new NP-completeness result concerning stubborn sets.

7

Analyzing and reducing simultaneous firing in signal-event nets

Roch S.

Fundamenta Informaticae

|

2000

|

Vol. 43, Nr 1-4

321-330

EN

Signal-event nets provide a modular modeling technique based on Petri nets. Actions of a module can be activated or can be prevented by another module through condition arcs. One-sided synchronization of modules is done by signal-events, which cause the execution of actions in steps. But due to condition arcs and signal-events simultaneous firing of steps may lead to markings, which are not reachable by conventional sequential interleaving. We give a criterion, in which situations simultaneous firing of steps can be safely omitted, without missing reachable markings.

8

Finding symmetries of algebraic system nets

Junttila T.A.

Fundamenta Informaticae

|

1999

|

Vol. 37, Nr 3

269-289

EN

The problem of finding symmetry information from algebraic system nets prior to the reach-ability graph generation is studied. The approach presented is based on wellformedness of transition descriptions, meaning that some data types in a net may be used in a symmetric way. Permutations on the domains of such data types produce symmetries on the state space level of the net, which in turn can be exploited during the reachability analysis. To ensure that the transitions behave symmetrically with respect to the chosen data domain permutations, a sufficient compatibility condition between data domain permutations and the algebraic terms used as transition guards and arc annotations is proposed. The solution is a general and flexi-ble one as it does not fix the set of applicable operations, enabling the design of customized net classes. To help the process of deciding whether a term is compatible with a data domain permutation, an approximation rule for the compatibility condition is given.