Fundamental techniques for the scalable analysis of systems
Abstract: This thesis introduces three fundamental techniques for the analysis of systems.
A new algorithm for the automatic parameter synthesis in stochastic systems.
The algorithm performs a search in the parameter domain and integrates precise but slow stochastic simulation and less precise but fast approximation techniques.
During the search, the algorithm uses a fast approximation technique as long as the search stays within the same region in the parameter domain, and only applies the precise stochastic simulation if a new region in the parameter domain is entered.
A new minimization algorithm for a specific class of visibly pushdown automata.
The class is general, and the motivation for the class stems from its use in trace abstraction.
Trace abstraction is an approach to verify programs with procedures.
In this context, minimization is crucial to circumvent the state explosion problem.
The algorithm reduces the minimization of the automaton to the synthesis of an appropriate equivalence relation.
The synthesis of an appropriate equivalence relation reduces to finding a maximal satisfying assignment to a Boolean formula.
A new algorithm for reachability analysis of continuous systems with linear dynamics and nondeterministic inputs (LTI systems).
The achievement of the algorithm is to integrate set-based operations and linear algebra operations in such a way that the application of the (notoriously costly) set operations is restricted to low dimensions.
To summarize, we present three techniques for the scalable analysis of systems.
The techniques are proven to be effective in advancing the state of the art
Abstract: Diese Dissertation stellt drei fundamentale Techniken zur Analyse von Systemen vor.
Ein neuer Algorithmus zur automatischen Parametersynthese in stochastischen Systemen.
Der Algorithmus führt eine Parametersuche durch, wobei er präzise, aber langsame stochastische Simulation und weniger präzise, aber schnelle Approximationstechniken integriert.
Für diese Suche wird solange eine schnelle Approximationstechnik verwendet, wie sich die Suche in derselben Region im Parameterraum bewegt.
Nur wenn eine neue Region betreten wird, wird die präzise stochastische Simulation eingesetzt.
Ein neuer Minimierungsalgorithmus für eine Klasse von Visibly Pushdown-Automaten.
Die Automatenklasse ist motiviert durch ihre Verwendung in Trace Abstraction, einer Verifikationsmethode für Programme mit Prozeduren.
Minimierung ist entscheidend, um die kombinatorische Explosion des Zustandsraums zu umgehen.
Der Algorithmus reduziert die Automatenminimierung auf die Synthese einer geeigneten Äquivalenzrelation.
Die Synthese erfolgt durch das Finden einer maximal erfüllenden Belegung für eine aussagenlogische Formel.
Ein neuer Algorithmus zur Erreichbarkeitsanalyse von kontinuierlichen Systemen mit linearer Dynamik und Nichtdeterminismus (sog. LTI-Systeme).
Der Algorithmus integriert Mengenoperation und Operationen aus der linearen Algebra derart, dass die Anwendung der (notorisch teuren) Mengenoperationen in niedrigen Dimensionen durchgeführt wird.
Zusammenfassend zeigen wir in dieser Dissertation drei Verfahren zur skalierbaren Analyse von Systemen, die den aktuellen Stand der Technik weiterentwickeln
- Location
-
Deutsche Nationalbibliothek Frankfurt am Main
- Extent
-
Online-Ressource
- Language
-
Englisch
- Notes
-
Universität Freiburg, Dissertation, 2018
- Keyword
-
Machine theory
Parameterschätzung
Automatentheorie
Verifikation
Lineares zeitinvariantes System
Erreichbarkeitsmenge
- Event
-
Veröffentlichung
- (where)
-
Freiburg
- (who)
-
Universität
- (when)
-
2018
- Creator
- DOI
-
10.6094/UNIFR/16396
- URN
-
urn:nbn:de:bsz:25-freidok-163963
- Rights
-
Kein Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Last update
-
21.03.0002, 8:06 AM CET
Data provider
Deutsche Nationalbibliothek. If you have any questions about the object, please contact the data provider.
Associated
Time of origin
- 2018
Other Objects (12)
Fundamental algorithmic techniques for distributed computations in networks : : information dissemination and maximum matching
Scalable 3D deep learning: methods and applications
Analysis of partial order reduction techniques for automated planning
The local fundamental group of a Kawamata log terminal singularity is finite
Internet-based behavioral activation for depression: systematic review and meta-analysis
Chemotherapy-induced peripheral neuropathy: longitudinal analysis of predictors for postural control
Laparoscopic video analysis using temporal, attention, and multi-feature fusion based-approaches
Scalable extracorporeal gas exchange device for medical applications : = Skalierbares extrakorporales Gasaustauschsystem für medizinische Anwendungen
Scalable visual analytics : solutions and techniques for business applications
Scalable String and Suffix Sorting: Algorithms, Techniques, and Tools
Digital image correlation techniques for motion analysis and biomechanical characterization of plants
Editorial: Integration of multi-omics techniques in cancer
Fundamental algorithmic techniques for distributed computations in networks : : information dissemination and maximum matching
Scalable 3D deep learning: methods and applications
Analysis of partial order reduction techniques for automated planning
The local fundamental group of a Kawamata log terminal singularity is finite
Internet-based behavioral activation for depression: systematic review and meta-analysis
Chemotherapy-induced peripheral neuropathy: longitudinal analysis of predictors for postural control
Laparoscopic video analysis using temporal, attention, and multi-feature fusion based-approaches
Scalable extracorporeal gas exchange device for medical applications : = Skalierbares extrakorporales Gasaustauschsystem für medizinische Anwendungen
Scalable visual analytics : solutions and techniques for business applications
Scalable String and Suffix Sorting: Algorithms, Techniques, and Tools
Digital image correlation techniques for motion analysis and biomechanical characterization of plants
Editorial: Integration of multi-omics techniques in cancer
Fundamental algorithmic techniques for distributed computations in networks : : information dissemination and maximum matching
Scalable 3D deep learning: methods and applications
Analysis of partial order reduction techniques for automated planning
The local fundamental group of a Kawamata log terminal singularity is finite
Internet-based behavioral activation for depression: systematic review and meta-analysis
Chemotherapy-induced peripheral neuropathy: longitudinal analysis of predictors for postural control
Laparoscopic video analysis using temporal, attention, and multi-feature fusion based-approaches
Scalable extracorporeal gas exchange device for medical applications : = Skalierbares extrakorporales Gasaustauschsystem für medizinische Anwendungen
Scalable visual analytics : solutions and techniques for business applications
Scalable String and Suffix Sorting: Algorithms, Techniques, and Tools
Digital image correlation techniques for motion analysis and biomechanical characterization of plants