@article{MaximovaGieseKrause2018,
  author    = {Maximova, Maria and Giese, Holger and Krause, Christian},
  title     = {Probabilistic timed graph transformation systems},
  series = {Journal of Logical and Algebraic Methods in Programming},
  volume    = {101},
  journal   = {Journal of Logical and Algebraic Methods in Programming},
  publisher = {Elsevier},
  address   = {New York},
  issn      = {2352-2208},
  doi       = {10.1016/j.jlamp.2018.09.003},
  pages     = {110 -- 131},
  year      = {2018},
  abstract  = {Today, software has become an intrinsic part of complex distributed embedded real-time systems. The next generation of embedded real-time systems will interconnect the today unconnected systems via complex software parts and the service-oriented paradigm. Due to these interconnections, the architecture of systems can be subject to changes at run-time, e.g. when dynamic binding of service end-points is employed or complex collaborations are established dynamically. However, suitable formalisms and techniques that allow for modeling and analysis of timed and probabilistic behavior of such systems as well as of their structure dynamics do not exist so far. To fill the identified gap, we propose Probabilistic Timed Graph Transformation Systems (PTGTSs) as a high-level description language that supports all the necessary aspects of structure dynamics, timed behavior, and probabilistic behavior. We introduce the formal model of PTGTSs in this paper as well as present and formally verify a mapping of models with finite state spaces to probabilistic timed automata (PTA) that allows to use the PRISM model checker to analyze PTGTS models with respect to PTCTL properties. (C) 2018 Elsevier Inc. All rights reserved.},
  language  = {en}
}
@book{GieseMaximovaSakizloglouetal.2018,
  author    = {Giese, Holger and Maximova, Maria and Sakizloglou, Lucas and Schneider, Sven},
  title     = {Metric temporal graph logic over typed attributed graphs},
  number    = {123},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-433-3},
  issn      = {1613-5652},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-411351},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {29},
  year      = {2018},
  abstract  = {Various kinds of typed attributed graphs are used to represent states of systems from a broad range of domains. For dynamic systems, established formalisms such as graph transformations provide a formal model for defining state sequences. We consider the extended case where time elapses between states and introduce a logic to reason about these sequences. With this logic we express properties on the structure and attributes of states as well as on the temporal occurrence of states that are related by their inner structure, which no formal logic over graphs accomplishes concisely so far. Firstly, we introduce graphs with history by equipping every graph element with the timestamp of its creation and, if applicable, its deletion. Secondly, we define a logic on graphs by integrating the temporal operator until into the well-established logic of nested graph conditions. Thirdly, we prove that our logic is equally expressive to nested graph conditions by providing a suitable reduction. Finally, the implementation of this reduction allows for the tool-based analysis of metric temporal properties for state sequences.},
  language  = {en}
}