@misc{RazzaqKaminskiRomeroetal.2018,
  author    = {Razzaq, Misbah and Kaminski, Roland and Romero, Javier and Schaub, Torsten H. and Bourdon, Jeremie and Guziolowski, Carito},
  title     = {Computing diverse boolean networks from phosphoproteomic time series data},
  series = {Computational Methods in Systems Biology},
  volume    = {11095},
  journal   = {Computational Methods in Systems Biology},
  publisher = {Springer},
  address   = {Berlin},
  isbn      = {978-3-319-99429-1},
  issn      = {0302-9743},
  doi       = {10.1007/978-3-319-99429-1_4},
  pages     = {59 -- 74},
  year      = {2018},
  abstract  = {Logical modeling has been widely used to understand and expand the knowledge about protein interactions among different pathways. Realizing this, the caspo-ts system has been proposed recently to learn logical models from time series data. It uses Answer Set Programming to enumerate Boolean Networks (BNs) given prior knowledge networks and phosphoproteomic time series data. In the resulting sequence of solutions, similar BNs are typically clustered together. This can be problematic for large scale problems where we cannot explore the whole solution space in reasonable time. Our approach extends the caspo-ts system to cope with the important use case of finding diverse solutions of a problem with a large number of solutions. We first present the algorithm for finding diverse solutions and then we demonstrate the results of the proposed approach on two different benchmark scenarios in systems biology: (1) an artificial dataset to model TCR signaling and (2) the HPN-DREAM challenge dataset to model breast cancer cell lines.},
  language  = {en}
}
@article{JoergesMargariaSteffen2011,
  author    = {J{\"o}rges, Sven and Margaria, Tiziana and Steffen, Bernhard},
  title     = {Assuring property conformance of code generators via model checking},
  series = {Formal aspects of computing : the international journal of formal methods},
  volume    = {23},
  journal   = {Formal aspects of computing : the international journal of formal methods},
  number    = {5},
  publisher = {Springer},
  address   = {New York},
  issn      = {0934-5043},
  doi       = {10.1007/s00165-010-0169-9},
  pages     = {589 -- 606},
  year      = {2011},
  abstract  = {Automatic code generation is an essential cornerstone of today's model-driven approaches to software engineering. Thus a key requirement for the success of this technique is the reliability and correctness of code generators. This article describes how we employ standard model checking-based verification to check that code generator models developed within our code generation framework Genesys conform to (temporal) properties. Genesys is a graphical framework for the high-level construction of code generators on the basis of an extensible library of well-defined building blocks along the lines of the Extreme Model-Driven Development paradigm. We will illustrate our verification approach by examining complex constraints for code generators, which even span entire model hierarchies. We also show how this leads to a knowledge base of rules for code generators, which we constantly extend by e.g. combining constraints to bigger constraints, or by deriving common patterns from structurally similar constraints. In our experience, the development of code generators with Genesys boils down to re-instantiating patterns or slightly modifying the graphical process model, activities which are strongly supported by verification facilities presented in this article.},
  language  = {en}
}