PD Dr. Louchka Popova-Zeugmann

PD Dr. Popova-Zeugmann erforscht die formale Modellierung und Verifikation von verteilten, zeitabhängigen Systemen mittels Petri-Netzen — insbesondere wie man durch Prioritäten und Zeitbeschränkungen das Verhalten solcher Netze kontrolliert und stabilisiert. Ihr aktueller Fokus liegt auf der Entwicklung von Semantiken und Analysemethoden für zeitgesteuerte Petri-Netze, um Eigenschaften wie Lebendigkeit und Beschränktheit zu sichern. Diese Arbeiten adressieren konkrete Anforderungen in Workflow-Management, eingebetteten Systemen und bioinformatischen Modellen, wo unkontrolliertes oder unbegrenztes Systemverhalten zu Fehlern oder Instabilität führt. Die Methoden ermöglichen es, komplexe nebenläufige Prozesse formal zu verifizieren, bevor sie in kritischen Anwendungen eingesetzt werden.

🔒 Das System hat 318 mögliche Industrie-Partner gefunden — Firmen, Scores und Begründungen sind nur für eingeloggte Nutzer:innen sichtbar. Anmelden

• Vergleichende Analyse und Verifikation für Verteilte Sicherheitskritische Systeme (CAVER)

  Quelle ↗

  Förderer: DFG Sachbeihilfe Zeitraum: 10/2015 - 07/2017 Projektleitung: PD Dr. Louchka Popova-Zeugmann

• Time and Petri Nets

  2013

  DOI

• On Time Petri Nets.

  1991

  Journal of automata, languages and combinatorics

• Time Petri Nets for Modelling and Analysis of Biochemical Networks

  2005

  Biochemical networks are modelled at different abstraction levels. Basically, qualitative and quantitative models can be distinguished, which are typically treated as separate ones. In this paper, we bridge the gap between qualitative and quantitative models and apply time Petri nets for modelling and analysis of molecular biological systems. We demonstrate how to develop quantitative models of biochemical networks in a systematic manner, starting from the underlying qualitative ones. For this purpose we exploit the well-established structural Petri net analysis technique of transition invariants, which may be interpreted as a characterisation of the system?s steady state behaviour. For the analysis of the derived quantitative model, given as time Petri net, we present structural techniques to decide the time-dependent realisability of a transition sequence and to calculate its shortest and longest time length. All steps of the demonstrated approach consider systems of integer linear inequalities. The crucial point is the total avoidance of any state space construction. Therefore, the presented technology may be applied also to infinite systems, i.e. unbounded Petri nets.