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

Metoda wyznaczania średniego czasu dojścia do stanu pochłaniającego jednorodnego łańcucha Markowa

Kwiatkowski W.

Biuletyn Instytutu Automatyki i Robotyki

|

2012

|

R. 18, nr 33

3-15

PL

Rozpatrywany jest jednorodny łańcuch Markowa o wielu stanach pochłaniających. Przedstawiona jest metoda wyznaczania średniego czasu dojścia do wybranego stanu pochłaniającego. Metoda oparta jest na rozszerzeniu zadanego łańcucha Markowa o nowe stany. Dla łańcucha rozszerzonego definiowana jest funkcja wypłat towarzysząca tranzycjom. Szczególne podejście do analitycznego rozwiązania problemu związane jest z zależnością wypłaty nie tylko od tranzycji, ale także od czasu. Rozpatrywane w artykule zadanie pojawia się przy projektowaniu interfejsów, protokołów, planowania etapowych przedsięwzięć o charakterze transportowym, produkcyjnym itp.

EN

A homogeneous Markov chain with many absorbing states is considered. A method to obtain an average time to reach a selected absorbing state is presented. The method is based on an extension of the given Markov chain with new states. For the extended Markov chain a reward function associated with transitions is defined. A particular approach to the analytical solution of the problem is based on the dependence of rewards not only on transitions, but also on time. The task considered in this paper emerges during the design of interfaces, protocols, planning of staged transport or production projects etc.

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.