theses.bib

@phdthesis{jdq13,
  title = {{S}imilarity, {L}ogic, and {G}ames - {B}ridging {M}odeling {L}ayers of {H}ybrid {S}ystems},
  author = {{J}an-{D}avid {Q}uesel},
  url = {http://www.cs.cmu.edu/~jquesel/paper/diss.pdf},
  school = {University of Oldenburg},
  year = 2013,
  abstract = {
	Specifications and implementations of complex physical systems tend to differ as low-level effects such as sampling are often ignored when high-level models are created. Thus, the low-level models are often not exact refinements of the high-level specification. However, intuitively we would consider them as similar. To bridge the gap between these models, we study notions of similarity and robust refinement relations for hybrid systems. 
	We identify a family of such relations which permit certain bounded deviations in the behavior of a system specification and its implementation in both values of the system variables and timings. We show that for this relaxed version of refinement a broad class of properties is preserved. This includes stability, safety, as well as bounded response properties. The question whether two systems are in refinement relation can be reduced to a reachability problem for hybrid games.
\\
	For the study of parametric hybrid games, we propose a new logic, called \emph{differential dynamic game logic}~(dDGL), and develop a theorem prover for it.  We give an operational and a modal semantics of dDGL and prove their equivalence.  To allow for deductive reasoning, we exploit the fact that dDGL is a conservative extension of differential dynamic logic~(dL). Subsequently, we provide rules for extending the dL sequent proof calculus to handle the dDGL specifics.  Furthermore, we have implemented dDGL in our theorem prover KeYmaera. We demonstrate the strength of dDGL by applying KeYmaera to a case study in which a robot plays a game against other agents in a factory automation scenario. 
\\
	KeYmaera is a theorem prover for hybrid system verification. It reduces the verification task to smaller subtasks that can be decided by quantifier elimination. Unfortunately, quantifier elimination over the reals is doubly exponential in the number of quantifier alternations already in theory and even in the number of variables in many implementations.  Therefore, we compare different implementations of procedures for quantifier elimination and alternative methods for dealing with these subtasks.
\\
	We show that our dDGL-based approach for proving that two hybrid systems are in robust refinement relation can be effectively used. For this, we present a case study from the domain of train control with a safe specification using instantaneous and imperfect implementations which suffer from communication delays.
	}
}

@mastersthesis{jdq07,
  title = {{A} {T}heorem {P}rover for {D}ifferential {D}ynamic {L}ogic: {D}eductive {V}erification of {H}ybrid {S}ystems},
  author = {{J}an-{D}avid {Q}uesel},
  url = {http://www.cs.cmu.edu/~jquesel/paper/quesel07.pdf},
  school = {University of Oldenburg},
  year = 2007,
  abstract = {
	This thesis aims at the computer aided verification of hybrid systems using deductive techniques. We have developed an interactive verification tool on the basis of a sound sequent calculus for dL. The logic dL is a dynamic logic with a special focus on the specification and verification of hybrid systems. Our implementation extends the theorem prover component of the KeY~system with rules and data structures for handling dL formulas. Additionally, we have integrated KeY with the computer algebra system Mathematica to handle quantifiers over the reals and real arithmetic. In order to demonstrate that our implementation can be used for verifying larger systems, we prove safety in a case study from the context of the European Train Control System (ETCS). 
	}
}

@misc{jdq05,
  title = {{M}o{D}i{S}h{C}a - {M}odel {C}hecking {D}iscrete {S}hape {C}alculus},
  author = {{J}an-{D}avid {Q}uesel},
  url = {http://www.cs.cmu.edu/~jquesel/paper/quesel05.pdf},
  school = {University of Oldenburg},
  year = 2005,
  abstract = {
	This thesis describes how a decidable fragment of the Shape Calculus, an extended Duration Calculus, can be translated into WS1S. WS1S is the monadic second order logic with one successor. We generalise a translation for the two dimensional case to an arbitrary number of dimensions and beyond an implementation of it will be presented: MoDiShCa.
Also we will illustrate how this tool can be used to verify complex systems by presenting a case study.
	}
}