Academic literature on the topic 'Reachability Parameter'
Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles
Consult the lists of relevant articles, books, theses, conference reports, and other scholarly sources on the topic 'Reachability Parameter.'
Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.
You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.
Journal articles on the topic "Reachability Parameter"
1
Cassez, Franck, Peter Gjøl Jensen, and Kim Guldstrand Larsen. "Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction*." Fundamenta Informaticae 178, no. 1-2 (2021): 31–57. http://dx.doi.org/10.3233/fi-2021-1997.
Full textAbstract:
We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. All of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.
2
Dirr, Gunther, and Michael Schönlein. "Uniform and L-ensemble reachability of parameter-dependent linear systems." Journal of Differential Equations 283 (May 2021): 216–62. http://dx.doi.org/10.1016/j.jde.2021.02.032.
Full text
3
Islam, Md Ariful, Rance Cleaveland, Flavio H. Fenton, Radu Grosu, Paul L. Jones, and Scott A. Smolka. "Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans." Theoretical Computer Science 765 (April 2019): 158–69. http://dx.doi.org/10.1016/j.tcs.2018.02.005.
Full text
4
Koutris, Paraschos, and Shaleen Deep. "The Fine-Grained Complexity of CFL Reachability." Proceedings of the ACM on Programming Languages 7, POPL (2023): 1713–39. http://dx.doi.org/10.1145/3571252.
Full textAbstract:
Many problems in static program analysis can be modeled as the context-free language (CFL) reachability problem on directed labeled graphs. The CFL reachability problem can be generally solved in time O ( n 3 ), where n is the number of vertices in the graph, with some specific cases that can be solved faster. In this work, we ask the following question: given a specific CFL, what is the exact exponent in the monomial of the running time? In other words, for which cases do we have linear, quadratic or cubic algorithms, and are there problems with intermediate runtimes? This question is inspired by recent efforts to classify classic problems in terms of their exact polynomial complexity, known as fine-grained complexity. Although recent efforts have shown some conditional lower bounds (mostly for the class of combinatorial algorithms), a general picture of the fine-grained complexity landscape for CFL reachability is missing. Our main contribution is lower bound results that pinpoint the exact running time of several classes of CFLs or specific CFLs under widely believed lower bound conjectures (e.g., Boolean Matrix Multiplication, k -Clique, APSP, 3SUM). We particularly focus on the family of Dyck- k languages (which are strings with well-matched parentheses), a fundamental class of CFL reachability problems. Remarkably, we are able to show a Ω( n 2.5 ) lower bound for Dyck-2 reachability, which to the best of our knowledge is the first super-quadratic lower bound that applies to all algorithms, and shows that CFL reachability is strictly harder that Boolean Matrix Multiplication. We also present new lower bounds for the case of sparse input graphs where the number of edges m is the input parameter, a common setting in the database literature. For this setting, we show a cubic lower bound for Andersen’s Pointer Analysis which significantly strengthens prior known results.
5
Wu, Di, and Xenofon Koutsoukos. "Reachability analysis of uncertain systems using bounded-parameter Markov decision processes." Artificial Intelligence 172, no. 8-9 (2008): 945–54. http://dx.doi.org/10.1016/j.artint.2007.12.002.
Full text
6
Arias, Jaime, Kyungmin Bae, Carlos Olarte, Peter Csaba Ölveczky, and Laure Petrucci. "A Rewriting-logic-with-SMT-based Formal Analysis and Parameter Synthesis Framework for Parametric Time Petri Nets." Fundamenta Informaticae 192, no. 3-4 (2024): 261–312. http://dx.doi.org/10.3233/fi-242195.
Full textAbstract:
This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the “standard” semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and complete formal analyses for PITPNs. We develop and implement a new general folding approach for symbolic reachability, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite. Our work opens up the possibility of using the many formal analysis capabilities of Maude—including full LTL model checking, analysis with user-defined execution strategies, and even statistical model checking—for such nets. We illustrate this by explaining how almost all formal analysis and parameter synthesis methods supported by the state-of-the-art PITPN tool Roméo can be performed using Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments show that our methods outperform Roméo in many cases.
7
Geng, Jie, Ying Li, Hailong Guo, Huan Zhang, and Chuan Lv. "Spatial Data-Based Automatic and Quantitative Approach in Analyzing Maintenance Reachability." Applied Sciences 12, no. 24 (2022): 12804. http://dx.doi.org/10.3390/app122412804.
Full textAbstract:
Reachability, as a vital parameter in product maintainability design, exerts a tremendous influence in practical maintenance, especially in the usage stage. To decrease subjectivity in maintenance reachability analysis, this study proposes an automatic and quantitative approach based on the spatial data of the human arm to implement maintenance reachability analysis. The approach focused on two aspects, namely, accuracy and efficiency. In terms of accuracy, the presented methodology starts from the maintenance spot where the human hand is attached. An original global data sequence set was generated, including the wrist, elbow, and shoulder joints, under the constraints of kinematics, in which a data sequence represents an arm motion. Moreover, the surrounding objects are represented by their geometric data, in which each data sequence is analyzed to judge whether collision occurs between arm segments and surrounding objects. In this filtering process, the data sequence is retained if the aforementioned collision does not occur. In terms of efficiency, owing to the large number of global data sequences, the efficiency of the interval selection in collision calculation is also taken into consideration in this methodology. Unlike the traditional methods in the virtual environment, the starting point is the maintenance spot, rather than the human body. Hence, nearly all possibilities of arm postures are considered in a global perspective with little subjective involvement, which enhances the automation and objectivity in maintenance reachability analysis to a certain extent. The case study shows the usability and feasibility by a practical maintenance scene.
8
Kumar, Alok, Bhagyashree Umathe, and Atul Kelkar. "A Koopman Reachability Approach for Uncertainty Analysis in Ground Vehicle Systems." Machines 12, no. 11 (2024): 753. http://dx.doi.org/10.3390/machines12110753.
Full textAbstract:
Recent progress in autonomous vehicle technology has led to the development of accurate and efficient tools for ensuring safety, which is crucial for verifying the reliability and security of vehicles. These vehicles operate under diverse conditions, necessitating the analysis of varying initial conditions and parameter values. Ensuring the safe operation of the vehicle under all these varying conditions is essential. Reachability analysis is an important tool to certify the safety and stability of the vehicle dynamics. We propose a reachability analysis approach for evaluating the response of the vehicle dynamics, specifically addressing uncertainties in the initial states and model parameters. Reachable sets illustrate all the possible states of a dynamical system that can be obtained from a given set of uncertain initial conditions. The analysis is crucial for understanding how variations in initial conditions or system parameters can lead to outcomes such as vehicle collisions or deviations from desired paths. By mapping out these reachable states, it is possible to design systems that maintain safety and reliability despite uncertainties. These insights help to ensure the stability and reliability of the vehicles, even in unpredictable conditions, by reducing accidents and optimizing performance. The nonlinearity of the model complicates the computation of reachable sets in vehicle dynamics. This paper proposes a Koopman theory-based approach that utilizes the Koopman principal eigenfunctions and the Koopman spectrum. By leveraging the Koopman principal eigenfunction, our method simplifies the computational process and offers a formal approximation for backward and forward reachable sets. First, our method effectively computes backward and forward reachable sets for a nonlinear quarter-car model with fixed parameter values. Furthermore, we applied our approach to analyze the uncertainty response for cases with uncertain parameters of the vehicle model. When compared to time-domain simulations, our proposed Koopman approach provided accurate results and also reduced the computational time by half in most cases. This demonstrates the efficiency and reliability of our proposed approach in dynamic systems uncertainty analysis using the reachable sets.
9
Huu Sach, Pham. "Reachability for discrete-time dynamical set-valued systems depending on a parameter." Optimization 48, no. 1 (2000): 17–42. http://dx.doi.org/10.1080/02331930008844492.
Full text
10
Qian, Moshu, Guanghua Zhong, Xinggang Yan, Heyuan Wang, and Yang Cui. "A Closed-Loop Brain Stimulation Control System Design Based on Brain-Machine Interface for Epilepsy." Complexity 2020 (April 14, 2020): 1–15. http://dx.doi.org/10.1155/2020/3136715.
Full textAbstract:
In this study, a closed-loop brain stimulation control system scheme for epilepsy seizure abatement is designed by brain-machine interface (BMI) technique. In the controller design process, the practical parametric uncertainties involving cerebral blood flow, glucose metabolism, blood oxygen level dependence, and electromagnetic disturbances in signal control are considered. An appropriate transformation is introduced to express the system in regular form for design and analysis. Then, sufficient conditions are developed such that the sliding motion is asymptotically stable. Combining Caputo fractional order definition and neural network (NN), a finite time fractional order sliding mode (FFOSM) controller is designed to guarantee reachability of the sliding mode. The stability and reachability analysis of the closed-loop tracking control system gives the guideline of parameter selection, and simulation results based on comprehensive comparisons are carried out to demonstrate the effectiveness of proposed approach.
Dissertations / Theses on the topic "Reachability Parameter"
1
Zebiri, Hossni. "Hinf-Linear Parameter Varying Controllers Order Reduction : Application to semi-active suspension control." Thesis, Mulhouse, 2016. http://www.theses.fr/2016MULH7733/document.
Full textAbstract:
L'amélioration permanente de la qualité et des performances des systèmes automatiques constitue un défi majeur dans la théorie du contrôle. La théorieHinf a permis d'améliorer considérablement les performances des correcteurs. Ces derniers reposent sur des modèles mathématiques qui sont potentiellement d'ordre élevé (c.-à-d. comprenant un nombre élevé d'équations différentielles). De plus, l'ajout de poids de pondérations spécifiant les performances à respecter accroit encore plus leur ordre. La complexité algorithmique résultante peut alors rendre leur implantation difficile voire même impossible pour un fonctionnement en temps réel.Les travaux présentés visent à réduire l'ordre de correcteurs Hinf dans le but de faciliter leur intégration tout en respectant les performances imposées d'une part et proposent une majoration de l'erreur introduite par l'étape de réduction d'autre part.Dans la littérature, de nombreuses méthodes pour la réduction d'ordre de modèles et de correcteurs des systèmes LTI ont été développées. Ces techniques ont été étudiées, comparées et testées sur un ensemble de benchmarks. S'appuyant sur ces travaux, nous proposons une extension aux systèmes linéaires à paramètres variants (LPV). Pour valider leurs performances, une application sur une commande d'une suspension semi-active a montré l'efficacité des algorithmes de réduction développés<br>The work presented in this dissertation is related to the Hinf-LPV-controller orderReduction. This latter consists of the design of a robust reduced-order LPV-controller for LPV-systems. The order reduction issue has been very fairly investigated. However, the case of LPV-control design is slightly discussed. This thesis focuses primarily on two topics: How to obtain an LPV-reduced-order controller even the high order generated by the classical synthesis and how this reduced order controller can deal with a practical engineering problem (semi-active suspension control). In view of this, the order-reduction topic and the Hinf-synthesis theory have been widely studied in this thesis. This study, has allowed the development of a new method forH1-LPV-controller order reduction
2
Al, Khatib Mohammad. "Analyse de stabilité, ordonnancement, et synthèse des systèmes cyber-physiques." Thesis, Université Grenoble Alpes (ComUE), 2017. http://www.theses.fr/2017GREAM041/document.
Full textAbstract:
Il s'agit d'une étude menée sur les systèmes cyber-physiques sur trois aspects principaux: la vérification de la stabilité, l'ordonnancement et la synthèse des paramètres. Les systèmes de contrôle embarqués (ECS) agissant dans le cadre de contrats temporels sont la classe considérée de systèmes cyber-physiques dans la thèse. ECS fait référence à des intégrations d'un dispositif informatique avec le système physique. En ce qui concerne les contrats temporels, ils sont des contraintes de temps sur les instants où se produisent certains événements tels que l'échantillonnage, l'actionnement et le calcul. Ces contrats sont utilisés pour modéliser les problèmes qui se posent dans les systèmes de contrôle modernes: incertitudes sur les retards d'actionnement, les périodes d'échantillonnage incertaines et l'interaction de plusieurs systèmes physiques avec des ressources informatiques partagées (CPUs). Maintenant, compte tenu d'un ECS et d'un contrat temporel, nous reformulons le système de manière impulsionnelle et vérifions la stabilité du système, sous toutes les incertitudes bornées et données par le contrat, en utilisant des techniques d'approximation convexe et de nouveaux résultats généralisés pour le problème sur une classe de systèmes modélisés dans le cadre des inclusions différentielles. Deuxièmement, compte tenu d'un ensemble de contrôleurs implémentés sur une plate-forme de calcul commune (CPUs), dont chacun est soumis à un contrat de synchronisation, et à son meilleur et son plus mauvais cas d'exécution dans chaque CPU, nous synthétisons une politique d’ordonnancement dynamique qui garantit que chaque contrat temporel est satisfait et que chacun des CPU partagés est attribué à au plus un contrôleur à tout moment. L'approche est basée sur une reformulation qui nous permet d'écrire le problème d’ordonnancement comme un jeu temporelle avec spécification de sureté. Ensuite, en utilisant l'outil UPPAAL-TIGA, une solution au jeu fournit une politique d’ordonnancement appropriée. En outre, nous fournissons une nouvelle condition nécessaire et suffisante pour l’ordonnancement des tâches de contrôle en fonction d’un jeu temporisé simplifiés. Enfin, nous résolvons un problème de synthèse de paramètres qui consiste à synthétiser une sous-approximation de l'ensemble des contrats de synchronisation qui garantissent en même temps l’ordonnancement et la stabilité des contrôleurs intégrés. La synthèse est basée sur un nouveau paramétrage du contrat temporel pour les rendre monotones, puis sur un échantillonnage à plusieurs reprises de l'espace des paramètres jusqu'à atteindre une précision d'approximation prédéfinie<br>This is a study conducted on cyber-physical systems on three main aspects: stability verification, scheduling, and parameter synthesis. Embedded control systems (ECS) acting under timing contracts are the considered class of cyber-physical systems in the thesis. ECS refers to integrations of a computing device with the physical system. As for timing contracts they are time constraints on the instants where some events happen such as sampling, actuation, and computation. These contracts are used to model issues that arise in modern embedded control systems: uncertain sampling to actuation delays, uncertain sampling periods, and interaction of several physical systems with shared computational resources (CPUs). Now given an ECS and a timing contract we reformulate the system into an impulsive one and verifies stability of the system, under all possible bounded uncertainties given by the contract, using safe convex approximation techniques and new generalized results for the problem on a class of systems modeled in the framework of difference inclusions. Second given a set of controllers implemented on a common computational platform (CPUs), each of which is subject to a timing contract, and best and worst case execution times on each CPU, we synthesize a dynamic scheduling policy, which guarantees that each timing contract is satisfied and that each of the shared CPUs are allocated to at most one embedded controller at any time. The approach is based on a timed game formulation that allows us to write the scheduling problem as a timed safety game. Then using the tool UPPAAL-TIGA, a solution to the safety game provides a suitable scheduling policy. In addition, we provide a novel necessary and sufficient condition for schedulability of the control tasks based on a simplified timed game automaton. Last, we solve a parameter synthesis problem which consists of synthesizing an under-approximation of the set of timing contracts that guarantee at the same time the schedulability and stability of the embedded controllers. The synthesis is based on a re-parameterization of the timing contract to make them monotonic, and then on a repeatedly sampling of the parameter space until reaching a predefined precision of approximation
3
Hilaire, Mathieu. "Parity games and reachability in infinite-state systems with parameters." Electronic Thesis or Diss., université Paris-Saclay, 2022. http://www.theses.fr/2022UPASG095.
Full textAbstract:
Les approches standard de la vérification de modèle se limitent à des spécifications concrètes, par exemple «est-il possible d'atteindre une configuration après que plus de 10 unités de temps se soient écoulées?». Néanmoins, pour certains types de programmes informatiques, comme les technologies embarquées, les contraintes dépendent de l'environnement. De là émerge la nécessité des spécifications paramétriques, par exemple «est-il possible d'atteindre une configuration après que plus de p unités de temps se soient écoulées?» où p désigne un paramètre dont la valeur reste à spécifier.Dans cette thèse nous étudions des variantes paramétriques de trois modèles classique, les automates à pile, à compteur, et temporisés. En plus d'exprimer des contraintes concrètes (sur la pile, le compteur ou les horloges), ces modèles peuvent exprimer des contraintes paramétriques via des comparaisons avec des paramètres. Le problème de l'accessibilité consiste à demander s'il existe une assignation des paramètres telle que il existe une exécution acceptante dans l'automate concret qui en résulte. En plus de ce problème nous étudions des jeux de parités paramétriques, où deux joueurs choisissent une évaluation pour chaque paramètre chacun leur tour, puis déplacent un jeton dans le graphe de l'automate concret résultant. Nous nous intéressons au problème de décider quel joueur dispose d'une stratégie gagnante.Les automates temporisés paramétriques ont été introduit dans les années 90 par Alur, Henzinger et Vardi, qui ont démontré que le problème de l'accessibilité était indécidable, même avec seulement trois horloges pouvant être comparées à des paramètres, ou horloges paramétriques — mais décidable dans le cas d'une seule horloge paramétrique. Des résultats récents de Bundala et Ouaknine démontrent que dans le cas de deux horloges paramétriques et un paramètre, le problème est décidable ainsi que PSPACE^NEXP-dur. Un des principaux résultats de cette thèse consiste à démontrer le caractère EXPSPACE-complet du problème.La borne inférieure EXPSPACE repose sur des résultats récents du domaine de la complexité avancée. Inspirés par Göller, Haase, Ouaknine, et Worrell, nous visualisons la classe EXPSPACE comme un langage de feuille (vision qui repose sur le théorème de Barrington). Nous introduisons un langage de programmation qui peut reconnaître ce genre de langage de feuille. Nous utilisons ensuite une représentation des entiers sous forme de restes chinois dont Chiu, Davida et Litow ont montré qu'elle permettait de calculer en LOGSPACE la représentation binaire, et démontrons grâce à elle que les automates temporisés paramétriques à deux horloges paramétriques et un paramètre peuvent simuler notre langage de programmation.Pour la borne supérieure, à la façon de Bundala et Ouaknine, nous réduisons le problème au problème de l'accessibilité dans un type particulier d'automates à compteur paramétrique. Par une série de techniques de découpage d'une exécution fictive, nous démontrons que ce problème est dans PSPACE. Étant donné que notre réduction se fait en temps exponentiel, cela conduit à une borne supérieure EXPSPACE pour le problème de l'accessibilité dans les automates temporisés paramétriques à deux horloges et un paramètre.En ce qui concerne les jeux de parités paramétriques pour les automates à piles paramétriques, nous démontrons que le problème de déterminer quel joueur a une stratégie gagnante est dans (n+1)-EXP si le nombre de paramètres est fixé à n, mais nonélémentaire sinon. Le caractère nonélémentaire du problème est démontré par réduction du problème de la satisfaisabilité des formules de la logique du premier ordre. La borne supérieure est obtenue via une réduction aux automates à pile de piles, pour lesquels le problème des jeux de parités est n-EXP-complet dans le cas de n niveaux de piles<br>The most standard model checking approaches are limited to verifying concrete specifications, such as “can we reach a configuration with more than 10 time units elapsing ?”. Nethertheless, for certaincomputer programs, like embedded systems, the constraints depend on the environment. Thus arisesthe need for parametric specifications, such as “can we reach a configuration with more than p timeunits elapsing ?” where p is a parameter which takes values in the non-negative integers.In this thesis, we study parametric pushdown, counter and timed automata and extensions the-reof. In addition to expressing concrete constraints (on the stack, on the counter or on clocks), thesecan employ parametric constraints. The reachability problem for a parametric automaton asks for the existence of an assignment of the parameters such that there exists an accepting run in the underlying concrete automaton. In addition to the reachability problem, we consider parametric parity games, two player games where players alternate chosing assignments for each parameters, then alternate moving a token along the configurations of the concrete automaton resulting from their choice of parameter assignment. We consider the problem of deciding which player has a winning strategy.Parametric timed automata (PTA for short) were introduced in the 90s by Alur, Henzinger andVardi, who showed that the reachability problem for PTA was undecidable, already when only threeclocks can be compared against parameters, and decidable in the case only one clock can. We callsuch clocks that can be compared to parameters parametric clocks. A few years ago, Bundala andOuaknine proved that, for parametric timed automata with two parametric clocks and one parame-ter ((2, 1)-PTA for short), the reachability problem is decidable and also provided a PSPACENEXP lower bound. One of the main results of this thesis states that reachability for (2, 1)-PTA is in factEXPSPACE-complete. For the EXPSPACE lower bound, inspired by previous work by Göller, Haase, Ouaknine, and Worrell, we rely on a serializability characterization of EXPSPACE (in turn originally based on Barrington's Theorem). We provide a programming language and we show it can simulate serializability computations. Relying on a logspace translation of numbers in Chinese Remainder Representation to binary representation due to Chiu, Davida, and Litow, we then show that small (2, 1)-PTA can simulate our programming language. For the EXPSPACE upper bound on (2, 1)-PTA, we first give a careful exponential time reduction towards a variant of parametric one-counter automata over one parameter based on a minor adjustment of a construction due to Bundala and Ouaknine. We solve the reachability problem for this parametric one-counter automata with one parameter variant, by providing a series of techniques to partition a fictitious run into several carefully chosen subruns. This allows us to prove that it is sufficient to consider a parameter value of exponential magnitude only, which in turn leads to a doubly-exponential upper bound on the value of the only parameter of the (2, 1)-PTA. We hope that extensions of our techniques lead to finally establishing decidability of the long-standing open problem of reachability in PTA with two parametric clocks and arbitrarily many parameters.Concerning parametric pushdown automata, our main result states that deciding the winner ofa parametric parity game is in (n + 1)-EXP in the case the number of parameters n is fixed, but nonelementary otherwise. We provide the nonelementary lower bound via a reduction of the FO satisfiability problem on words. For the upper bound, we reduce parametric pushdown parity games to higher-order pushdown automata parity games, which are known to be n-EXP complete in the case of stacks of level n
4
Lu, Yu. "Etude du volume de travail des robots : enveloppe, atteignabilite." Paris, ENSAM, 1988. http://www.theses.fr/1988ENAM0002.
Full textAbstract:
Proposition d'une methode geometrique de construction de l'enveloppe atteignable d'un robot. En effet, la connaisance des volumes atteignables d'un robot permet de determiner la faisabilite d'une trajectoire, de faciliter le positionnement du robot dans sa cellule de travail et l'optimisation des parametres geometriques de conception du manipulateur. Creation d'un outil de simulation a partir d'une base graphique
5
Gomes, Maria Josiane Ferreira. "Propriedades de filtros lineares para sistemas lineares com saltos markovianos a tempo discreto." Universidade de São Paulo, 2015. http://www.teses.usp.br/teses/disponiveis/55/55134/tde-06042015-151704/.
Full textAbstract:
Este trabalho é dedicado ao estudo do erro de estimação em filtragem linear para sistemas lineares com parâmentros sujeitos a saltos markovianos a tempo discreto. Indroduzimos o conceito de alcançabilidade média para uma classe de sistemas. Construímos um conjunto de matrizes de alcançabilidade e mostramos que o conceito usual de alcan- çabilidade definido através da positividade do gramiano é caracterizado pela definição por posto completo destas matrizes. A alcançabilidade média funciona como condição necessária e suficiente para positividade do segundo momento do estado do sistema, resultado esse que auxilia na caracterização da positividade uniforme da matriz de covariância do erro de estimação. Abordamos a estabilidade de estimadores com a interpretação de que a covariância do erro permanece limitada na presença de erro de qualquer magnitude no modelo do ruído, que é uma característica relevante para aplicações. Apresentamos uma prova de que filtros markovianos são estáveis sempre que o segundo momento condicionado é positivo. Exemplos numéricos encontram-se inclusos.<br>This work studies linear filtering for discrete-time systems with Markov jump parameters. We introduce a notion of average reachability for these systems and present a set of matrices playing the role of reachability matrices, in the sense that their rank is full if and only if the system is average reachable. Reachability is also a sufficient condition for the second moment of the system to be positive. Uniform positiveness of the error covariance matrix is studied for general (possibly non-markovian) linear estimators, relying on the state second moment positiveness. Satbility of linear markovian estimators is also addressed, allowing to show that markovian estimators are stable whenever the system is reachable, with the interpretation that the error covariance remains bounded in the presence of error of any magnitude in the model of the noise, which is a relevant feature for applications. Numerical examples are included.
Book chapters on the topic "Reachability Parameter"
1
Badings, Thom S., Nils Jansen, Sebastian Junges, Marielle Stoelinga, and Matthias Volk. "Sampling-Based Verification of CTMCs with Uncertain Rates." In Computer Aided Verification. Springer International Publishing, 2022. http://dx.doi.org/10.1007/978-3-031-13188-2_2.
Full textAbstract:
AbstractWe employ uncertain parametric CTMCs with parametric transition rates and a prior on the parameter values. The prior encodes uncertainty about the actual transition rates, while the parameters allow dependencies between transition rates. Sampling the parameter values from the prior distribution then yields a standard CTMC, for which we may compute relevant reachability probabilities. We provide a principled solution, based on a technique called scenario-optimization, to the following problem: From a finite set of parameter samples and a user-specified confidence level, compute prediction regions on the reachability probabilities. The prediction regions should (with high probability) contain the reachability probabilities of a CTMC induced by any additional sample. To boost the scalability of the approach, we employ standard abstraction techniques and adapt our methodology to support approximate reachability probabilities. Experiments with various well-known benchmarks show the applicability of the approach.
2
Zetzsche, Georg. "Recent Advances on Reachability Problems for Valence Systems (Invited Talk)." In Lecture Notes in Computer Science. Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-89716-1_4.
Full textAbstract:
AbstractValence systems are an abstract model of computation that consists of a finite-state control and some storage mechanism. In contrast to traditional models, the storage mechanism is not fixed, but given as a parameter. This allows us to precisely state questions like: For which storage mechanisms is the reachability problem decidable?This survey reports on recent results that aim to understand the impact of the storage mechanism on decidability and complexity of several variants of the reachability problem. The considered problems are configuration reachability, model-checking first-order logic with reachability, and reachability under bounded context switching and scope-boundedness.
3
Dahlsen-Jensen, Mikael Bisgaard, Baptiste Fievet, Laure Petrucci, and Jaco van de Pol. "On-The-Fly Algorithm for Reachability in Parametric Timed Games." In Tools and Algorithms for the Construction and Analysis of Systems. Springer Nature Switzerland, 2024. http://dx.doi.org/10.1007/978-3-031-57256-2_10.
Full textAbstract:
AbstractParametric Timed Games (PTG) are an extension of the model of Timed Automata. They allow for the verification and synthesis of real-time systems, reactive to their environment and depending on adjustable parameters. Given a PTG and a reachability objective, we synthesize the values of the parameters such that the game is winning for the controller. We adapt and implement the On-The-Fly algorithm for parameter synthesis for PTG. Several pruning heuristics are introduced, to improve termination and speed of the algorithm. We evaluate the feasibility of parameter synthesis for PTG on two large case studies. Finally, we investigate the correctness guarantee of the algorithm: though the problem is undecidable, our semi-algorithm produces all correct parameter valuations “in the limit”.
4
Spel, Jip, Sebastian Junges, and Joost-Pieter Katoen. "Finding Provably Optimal Markov Chains." In Tools and Algorithms for the Construction and Analysis of Systems. Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-72016-2_10.
Full textAbstract:
AbstractParametric Markov chains (pMCs) are Markov chains with symbolic (aka: parametric) transition probabilities. They are a convenient operational model to treat robustness against uncertainties. A typical objective is to find the parameter values that maximize the reachability of some target states. In this paper, we consider automatically proving robustness, that is, an $$\varepsilon $$ ε -close upper bound on the maximal reachability probability. The result of our procedure actually provides an almost-optimal parameter valuation along with this upper bound.We propose to tackle these ETR-hard problems by a tight combination of two significantly different techniques: monotonicity checking and parameter lifting. The former builds a partial order on states to check whether a pMC is (local or global) monotonic in a certain parameter, whereas parameter lifting is an abstraction technique based on the iterative evaluation of pMCs without parameter dependencies. We explain our novel algorithmic approach and experimentally show that we significantly improve the time to determine almost-optimal synthesis.
5
André, Étienne, Giuseppe Lipari, Hoang Gia Nguyen, and Youcheng Sun. "Reachability Preservation Based Parameter Synthesis for Timed Automata." In Lecture Notes in Computer Science. Springer International Publishing, 2015. http://dx.doi.org/10.1007/978-3-319-17524-9_5.
Full text
6
Lime, Didier, Olivier H. Roux, and Charlotte Seidner. "Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets." In Application and Theory of Petri Nets and Concurrency. Springer International Publishing, 2019. http://dx.doi.org/10.1007/978-3-030-21571-2_22.
Full text
7
Jovanović, Aleksandra, Didier Lime, and Olivier H. Roux. "Synthesis of Bounded Integer Parameters for Parametric Timed Reachability Games." In Automated Technology for Verification and Analysis. Springer International Publishing, 2013. http://dx.doi.org/10.1007/978-3-319-02444-8_8.
Full text
8
Ochab, Magdalena, Krzysztof Puszynski, and Andrzej Swierniak. "Reachability of the Therapeutic Target in the Systems with Parameters Switch." In Bioinformatics and Biomedical Engineering. Springer International Publishing, 2016. http://dx.doi.org/10.1007/978-3-319-31744-1_51.
Full text
9
Su, Guoxin, and David S. Rosenblum. "Nested Reachability Approximation for Discrete-Time Markov Chains with Univariate Parameters." In Automated Technology for Verification and Analysis. Springer International Publishing, 2014. http://dx.doi.org/10.1007/978-3-319-11936-6_26.
Full text
10
Paul, Mridul, and Ajanta Das. "Service Level Agreements for Smart Healthcare in Cloud." In Virtual and Mobile Healthcare. IGI Global, 2020. http://dx.doi.org/10.4018/978-1-5225-9863-3.ch001.
Full textAbstract:
With the advancement of Cloud computing, the adoption of cloud service in various industries is fast increasing. This is evident in the healthcare domain where the adoption is on the rise recently. However, the research contribution in this domain has been limited to certain functions. While cloud can increase availability, reachability of services, it is critical to design the healthcare service before provisioning. Besides, it is important to formulate Service Level Agreements (SLAs) to ensure that consumers can get guaranteed service from the service provider. The objective of this paper is to design the cloud based smart services for patient diagnostics. This research specifically defines service architecture for patients, physicians and diagnostic centers. In order to measure the proposed services, metrics of each SLA parameter is described with its functional and non-functional requirements. This paper also explains a case study implementation of a basic patient service using Google App Engine.
Conference papers on the topic "Reachability Parameter"
1
Han, Tingting, Joost-Pieter Katoen, and Alexandru Mereacre. "Approximate Parameter Synthesis for Probabilistic Time-Bounded Reachability." In 2008 IEEE 29th Real-Time Systems Symposium (RTSS). IEEE, 2008. http://dx.doi.org/10.1109/rtss.2008.19.
Full text
2
Wetzlinger, Mark, Adrian Kulmburg, and Matthias Althoff. "Adaptive parameter tuning for reachability analysis of nonlinear systems." In HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control. ACM, 2021. http://dx.doi.org/10.1145/3447928.3456643.
Full text
3
Wetzlinger, Mark, Niklas Kochdumper, and Matthias Althoff. "Adaptive Parameter Tuning for Reachability Analysis of Linear Systems." In 2020 59th IEEE Conference on Decision and Control (CDC). IEEE, 2020. http://dx.doi.org/10.1109/cdc42340.2020.9304431.
Full text
4
Chou, Yi, and Sriram Sankaranarayanan. "Bayesian Parameter Estimation for Nonlinear Dynamics Using Sensitivity Analysis." In Twenty-Eighth International Joint Conference on Artificial Intelligence {IJCAI-19}. International Joint Conferences on Artificial Intelligence Organization, 2019. http://dx.doi.org/10.24963/ijcai.2019/791.
Full textAbstract:
We investigate approximate Bayesian inference techniques for nonlinear systems described by ordinary differential equation (ODE) models. In particular, the approximations will be based on set-valued reachability analysis approaches, yielding approximate models for the posterior distribution. Nonlinear ODEs are widely used to mathematically describe physical and biological models. However, these models are often described by parameters that are not directly measurable and have an impact on the system behaviors. Often, noisy measurement data combined with physical/biological intuition serve as the means for finding appropriate values of these parameters. Our approach operates under a Bayesian framework, given prior distribution over the parameter space and noisy observations under a known sampling distribution. We explore subsets of the space of model parameters, computing bounds on the likelihood for each subset. This is performed using nonlinear set-valued reachability analysis that is made faster by means of linearization around a reference trajectory. The tiling of the parameter space can be adaptively refined to make bounds on the likelihood tighter. We evaluate our approach on a variety of nonlinear benchmarks and compare our results with Markov Chain Monte Carlo and Sequential Monte Carlo approaches.
5
Sadeghzadeh, Arash, and Pierre-Loic Garoche. "Reachability Analysis of Linear Parameter-Varying Systems with Neural Network Controllers." In 2022 IEEE Conference on Control Technology and Applications (CCTA). IEEE, 2022. http://dx.doi.org/10.1109/ccta49430.2022.9966104.
Full text
6
Meeko Oishi and Elebeoba May. "Addressing biological circuit simulation accuracy: Reachability for parameter identification and initial conditions." In 2007 IEEE/NIH Life Science Systems and Applications Workshop. IEEE, 2007. http://dx.doi.org/10.1109/lssa.2007.4400907.
Full text
7
Narvaez-Aroche, Octavio, Andrew Packard, Pierre-Jean Meyer, and Murat Arcak. "Reachability Analysis for Robustness Evaluation of the Sit-to-Stand Movement for Powered Lower Limb Orthoses." In ASME 2018 Dynamic Systems and Control Conference. American Society of Mechanical Engineers, 2018. http://dx.doi.org/10.1115/dscc2018-9066.
Full textAbstract:
A sensitivity-based approach for computing over-approximations of reachable sets, in the presence of constant parameter uncertainty and a single initial state, is used to analyze a three-link planar robot modeling a Powered Lower Limb Orthosis and its user. Given the nature of the mappings relating the state and parameters of the system with the input, and output describing the trajectories of its Center of Mass, reachable sets for their respective spaces can be obtained relying on the sensitivities of the nonlinear closed-loop dynamics in the state space. These over-approximations are used to evaluate the worst-case performances of a finite time horizon linear-quadratic regulator for controlling the ascending phase of the Sit-To-Stand movement.
8
Klenk, Matthew, Johan de Kleer, Daniel G. Bobrow, Sungwook Yoon, John Hanley, and Bill Janssen. "Guiding and Verifying Early Design Using Qualitative Simulation." In ASME 2012 International Design Engineering Technical Conferences and Computers and Information in Engineering Conference. American Society of Mechanical Engineers, 2012. http://dx.doi.org/10.1115/detc2012-70710.
Full textAbstract:
Design of a system starts with functional requirements and expected contexts of use. Early design sketches create a topology of components that a designer expects can satisfy the requirements. The methodology described here enables a designer to test an early design qualitatively against qualitative versions of the requirements and environment. Components can be specified with qualitative relations of the output to inputs, and one can create similar qualitative models of requirements, contexts of use and the environment. No numeric parameter values need to be specified to test a design. Our qualitative approach (QRM) simulates the behavior of the design, producing an envisionment (graph of qualitative states) that represents all qualitatively distinct behaviors of the system in the context of use. In this paper, we show how the envisionment can be used to verify the reachability of required states, to identify implicit requirements that should be made explicit, and to provide guidance for detailed design. Furthermore, we illustrate the utility of qualitative simulation in the context of a topological design space exploration tool.
9
Andrade de Melo, Alexsander, and Mateus De Oliveira Oliveira. "Symbolic Solutions for Symbolic Constraint Satisfaction Problems." In 17th International Conference on Principles of Knowledge Representation and Reasoning {KR-2020}. International Joint Conferences on Artificial Intelligence Organization, 2020. http://dx.doi.org/10.24963/kr.2020/6.
Full textAbstract:
A fundamental drawback that arises when one is faced with the task of deterministically certifying solutions to computational problems in PSPACE is the fact that witnesses may have superpolynomial size, assuming that NP is not equal to PSPACE. Therefore, the complexity of such a deterministic verifier may already be super-polynomially lower-bounded by the size of a witness. In this work, we introduce a new symbolic framework to address this drawback. More precisely, we introduce a PSPACE-hard notion of symbolic constraint satisfaction problem where both instances and solutions for these instances are implicitly represented by ordered decision diagrams (i.e. read-once, oblivious, branching programs). Our main result states that given an ordered decision diagram D of length k and width w specifying a CSP instance, one can determine in time f(w,w')*k whether there is an ODD of width at most w' encoding a solution for this instance. Intuitively, while the parameter w quantifies the complexity of the instance, the parameter w' quantifies the complexity of a prospective solution. We show that CSPs of constant width can be used to formalize natural PSPACE hard problems, such as reachability of configurations for Turing machines working in nondeterministic linear space. For such problems, our main result immediately yields an algorithm that determines the existence of solutions of width w in time g(w)*n, where g:N->N is a suitable computable function, and n is the size of the input.
10
Wang, Wei, Zejiang Wang, Xinbo Chen, and Junmin Wang. "A Lateral Motion Planning Method for Automated Vehicles Based on Sinusoids." In ASME 2020 Dynamic Systems and Control Conference. American Society of Mechanical Engineers, 2020. http://dx.doi.org/10.1115/dscc2020-3115.
Full textAbstract:
Abstract For automated driving applications, exact motion planning is pivotal to obstacle-avoidance and local driving, particularly in sophisticated surroundings. Treating this problem from a differential geometric viewpoint aids in simplifying the control and planning processes. Different from the classic differential geometric methods that result in piece-wise solutions with both forward and backward moving, this paper explores the application of sinusoids in exact motion planning regarding both the positive/continuous speed requirements and the system non-holonomic constraint. By converting the vehicle kinematic model to a similar chained form, we apply sinusoidal inputs with biases to generate the reference trajectory and discuss the principles of parameter selection for a given lateral displacement. To overcome the extra constraint brought by l’Hospital rule, we introduce a pair of entry/leave transition periods to ensures an adjustable speed profile and design flexibility. The resulting trajectory reflects an strong applicability to lane-changing or evasive steering scenarios. Since the proposed method does not account for the small-time controllability because of the positive/continuous speed constraint, the reachability problem is further investigated. We provide an analytic estimation of the reachable area edge and compare it with the numerical simulation results. Finally, some indoor field-tests verified the feasibility of the proposed method.