@phdthesis{Steeg2000, author = {Steeg, Martin}, title = {RADD, raddstar - a rule based database schema ; compiler, evaluator, and optimizer}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-000000118}, school = {BTU Cottbus - Senftenberg}, year = {2000}, abstract = {The thesis discusses the problems of database development and maintenance, and presents an approach to conceptual tuning realized by conceptual design using the HERM/RADD notation. The RADD design tool has been designed in order to develope HERM specifications graphically. RADD adds semantics and operations to the design, which are not directly annotated on the graphical specification, such as "afunctional" dependencies and SQL operations and procedures. The RADD/raddstar system extends the graphical specification of the database schema with the posibility to specify the operations and with the invocations for transforming the schema, for evaluating transactions, and for optimizing the schema, each of which according the implicite requirements graphically modeled and the explicite requirements specified by means of the conceptual specification language (CSL). CSL is used as command line interface of the RADD/raddstar. The graphical RADD schema as well as the CSL specifications are compiled into terms of the RADD* data model by the system, such that these terms are used for further evaluation actions. The actions performed by the RADD/raddstar (schema transformation, transaction and cost evaluating, schema optimization) are based on rules, that can be developed and modified by the user using the CSL.}, subject = {Datenbankentwurf; Schemaevolution; Entity-Relationship-Datenmodell; Konzeptionelle Modellierung; Typinferenz}, language = {en} } @phdthesis{Fahr2008, author = {Fahr, Martin}, title = {Parasit{\"a}re W{\"a}rmefl{\"u}sse und Verunreinigungen in Reinstmetall-Fixpunktzellen der Internationalen Temperaturskala}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus-4639}, school = {BTU Cottbus - Senftenberg}, year = {2008}, abstract = {Die internationale Temperaturskala von 1990 wird im Bereich von -38,8344°C bis 961,78°C neben dem Wasser- und dem Quecksilber-Tripelpunkt durch Schmelz- und Erstarrungstemperaturen von Reinstmetallen definiert. Die Unsicherheiten bei der Darstellung und Weitergabe der Basiseinheit Kelvin des Internationalen Einheitensystems in diesem Bereich (und somit auch der Einheit Grad Celsius und aller abgeleiteten Einheiten) werden dominiert von den Unsicherheiten der Realisierung dieser Fixpunkte und diese wiederum von einem Beitrag, der vom Einfluss in den Metallen gel{\"o}ster Verunreinigungen herr{\"u}hrt und bis jetzt nur pauschal abgesch{\"a}tzt wurde. Zwar wird versucht, noch reineres Fixpunktmetall zu verwenden, aber wesentliche Verbesserungen bez{\"u}glich der Reproduzierbarkeit der Fixpunkttemperaturen k{\"o}nnen nur durch eine Korrektion dieser Beitr{\"a}ge erreicht werden. Voraussetzungen f{\"u}r diese Korrektion sind nicht nur eine chemische Spurenanalyse der Fixpunktmetalle mit Unsicherheiten und Detektionsgrenzen am aktuellen technischen Limit, sondern auch die Kenntnis der Auswirkungen jeder einzelnen Verunreinigung auf die Fixpunkttemperatur. Diese Abh{\"a}ngigkeit der Phasen{\"u}bergangstemperatur von der Konzentration der jeweiligen Verunreinigung wird auf Grund fehlender Kenntnisse im Bereich kleinster Konzentrationen von 10^-9 bis 10^-5 (mol/mol) experimentell durch gezielte Dotierung der Fixpunktmetalle bestimmt. Um die dargestellten Probleme grundlegend zu l{\"o}sen, wurden im Rahmen dieser Arbeit zwei verschiedene Fixpunktzelldesigns entwickelt. Beide erlauben eine Messung und Kontrolle des Drucks der Gasatmosph{\"a}re und sind außerdem wiederverschließbar, wodurch sie eine chemische Analyse des Fixpunktmaterials erm{\"o}glichen, das sich in der Zusammensetzung wesentlich von dem unterscheiden kann, mit dem die Zelle bef{\"u}llt worden ist. W{\"a}hrend der eine Zelltyp f{\"u}r Kalibrierzwecke konstruiert worden ist und den herk{\"o}mmlichen Zellen {\"a}hnelt, wurde der zweite Typ auf die Verwendung von deutlich weniger Fixpunktmetall hin optimiert, so dass er sich unter anderem gut f{\"u}r die erw{\"a}hnten Dotierungsexperimente eignet. Zun{\"a}chst allerdings bringen die Ver{\"a}nderungen im Design gegen{\"u}ber den {\"u}blichen Fixpunktzellen unvermeidlich eine Vergr{\"o}ßerung unerw{\"u}nschter parasit{\"a}rer W{\"a}rmefl{\"u}sse mit sich, welche als sogenannte thermische Effekte die gemessene Fixpunkttemperatur verf{\"a}lschen. Diese fallen bei der angestrebten Verwendung von h{\"o}chstreinem Fixpunktmetall relativ zu den anderen Einflussgr{\"o}ßen umso mehr ins Gewicht, deswegen wurde ihre Untersuchung zu einem weiteren Schwerpunkt der Arbeit. Dabei konnte ein Verfahren zur Quantifizierung und Korrektion und ein besseres Verst{\"a}ndnis dieser Effekte entwickelt werden, welche f{\"u}r Metallfixpunktzellen jeder Bauart n{\"u}tzlich sind. Im Ergebnis liegen die Unsicherheiten bei den Messungen mit den verkleinerten Zellen unver{\"a}ndert im Bereich weniger hundert Mikrokelvin. Die Zellen eignen sich daher sehr gut, die Beeinflussung der Phasen{\"u}bergangstemperatur der Metallfixpunkte durch die Dotierung mit anderen Elementen im Konzentrationsbereich von 10^-7 bis 10^-5 zu bestimmen. Bevor dies abschließend auch experimentell mit Untersuchungen an ausgew{\"a}hlten bin{\"a}ren Systemen gezeigt wird, werden thermodynamische Berechnungen dargestellt, die erstmals eine Vielzahl von m{\"o}glichen Verunreinigungen in den Fixpunktzellen ausschließen, so dass sich nicht nur die Anzahl zu untersuchender m{\"o}glicher Verunreinigungen in den Fixpunkten erheblich reduziert, sondern auch die Anzahl zu ber{\"u}cksichtigender Beitr{\"a}ge bei der angestrebten Korrektion der Fixpunkttemperaturen. Alles in allem steht nun eine Methodik zur Verf{\"u}gung, die Unsicherheit bei der Darstellung der internationalen Temperaturskala im industriell besonders wichtigen Bereich von -40°C bis 1000°C mindestens um den Faktor 3 zu reduzieren.}, subject = {Metall; Verunreinigung; W{\"a}rmestrom; Internationale Temperaturskala; Temperaturfixpunkte; ITS-90; Verunreinigungen in ultrahochreinen Metallen; Thermische Effekte; Strahlungstransport; Temperature fixed-points; ITS-90; Impurities in ultra-pure metals; Thermal effects; Radiation transport}, language = {de} } @phdthesis{Warnecke2009, author = {Warnecke, Martin}, title = {Optimierung der Instandhaltungsplanung mit genetischen Algorithmen unter Ber{\"u}cksichtigung des Speicherverhaltens bei der Verf{\"u}gbarkeitsprognose von Kraftwerksanlagen}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus-5961}, school = {BTU Cottbus - Senftenberg}, year = {2009}, abstract = {In Zeiten des liberalisierten Strommarktes muss sich der Kraftwerkserrichter und -betreiber die Wahl seiner Prim{\"a}renergie und die Auslegung jedes einzelnen Kraftwerks hinsichtlich Emissionen und last but not least die Errichtungs- und sp{\"a}teren Betriebskosten genau {\"u}berlegen. Simulationen unter der Annahme verschiedener Szenarien sind bei diesem Marktumfeld zwingend erforderlich. Das Spannungsfeld zwischen Errichtungskosten, davon teilweise abh{\"a}ngiger Verf{\"u}gbarkeit, Instandhaltungsphilosophie und Betriebskosten bildet die Motivation f{\"u}r die Instandhaltungsoptimierung und Simulationen zur Verf{\"u}gbarkeitsprognose, die Thema dieser Arbeit sind. Der Schwerpunkt dieser Arbeit liegt auf der Planung der zeitbezogenen Instandhaltungsstrategie, bei der die Inspektion der Komponente nach einer vorgeschriebenen Zeitspanne erfolgt, die sich aus den Betriebs- und Herstellererfahrungen ableitet. Diese Problemstellung ist besonders anspruchsvoll, weil es durch Synergieeffekte zu starken Wechselwirkungen der Komponenten untereinander kommt. So besitzt jede Komponente ihre eigene theoretisch optimale Inspektionsperiode, im Verbund kann es jedoch sein, dass es wegen Freischaltungen oder Stillstandszeiten g{\"u}nstiger ist, einige Komponenten gemeinsam instandzuhalten und dabei eine einzelne Baugruppe vorzuziehen oder zur{\"u}ckzustellen. Die hieraus entstehenden Wechselwirkungen bilden eine nichtlineare, gemischt-ganzzahlige Berechnungsvorschrift f{\"u}r die Kostenabsch{\"a}tzung. F{\"u}r die Optimierung dieser Instandhaltungsplanung wurde in der vorliegenden Arbeit ein neuer Ansatz entwickelt. Nachdem festgestellt wurde, dass klassische Optimierungsverfahren dieses Problem der Instandhaltungsoptimierung nicht zufriedenstellend l{\"o}sen k{\"o}nnen, wurde eine L{\"o}sung auf Basis von „Genetischen Algorithmen" entwickelt. Gleichzeitig zur Instandhaltungsoptimierung wurde aufbauend auf vorangegangenen Arbeiten am Lehrstuhl die Methodik der Verf{\"u}gbarkeitsprognose komplexer kraftwerkstechnischer Anlagen weiterentwickelt und um die neue Komponente "Speicher" (ggf. mit Verlusten) erweitert. Mit dem Speichermodell wird die Verhaltensweise eines Speichers in die aufwandsreduzierte Monte-Carlo-Methode integriert.}, subject = {Kraftwerk; Instandhaltung; Optimierung; Instandhaltung; Genetische Algorithmen; Verf{\"u}gbarkeit; Monte-Carlo-Methode; Kraftwerk; Maintenance; Genetic algorithms; Availability; Monte-Carlo-Method; Power plant}, language = {de} } @phdthesis{Ohlerich2009, author = {Ohlerich, Martin}, title = {Investigations of the physics potential and detector development for the ILC}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus-14409}, school = {BTU Cottbus - Senftenberg}, year = {2009}, abstract = {The International Linear Collider offers a lot of different interesting challenges concerning the physics of elementary particles as well as the development of accelerator and detector technologies. In this thesis, we investigate two rather separate topics - the precision measurement of the Higgs boson mass and of its coupling to the neutral gauge boson Z and the research and development of sensors for BeamCal, which is a sub-detector system of the ILC detector. After the Higgs boson has been found, it is important to determine its properties with high precision. We employ the Higgs-strahlung process for this purpose. A virtual Z boson is created in the electron-positron collisions, which emits a Higgs-boson while becoming on-shell. Using the so-called recoil technique, we determine the Higgs boson mass by reconstructing the Z boson momentum and using the center-of-mass energy of the colliding leptons. This technique allows to measure the Higgs boson mass without considering the Higgs boson decay, i.e. it can be applied even to a Higgs boson invisibly decaying. Monte-Carlo studies including a full detector simulation and a full event reconstruction were performed to simulate the impact of a realistic detector model on the precision of the Higgs boson mass and production cross-section measurement. Also, an analytical estimate of the influence of a given detector performance on the Higgs boson mass measurement uncertainty is given. We included a complete sample of background events predicted by the Standard Model, which may have a detector response similar to the signal events. A probabilistic method is used for the signal-background separation. Several other probabilistic methods were used to investigate and improve the measurement of the Higgs-strahlung cross-section and the Higgs boson mass from the recoil mass spectrum obtained after the signal-background separation. For a Higgs boson mass of 120 GeV, a center-of-mass energy of 250 GeV and an integrated luminosity of 50/fb, a relative uncertainty of 10\% is obtained for the cross-section measurement, and a precision of 118 MeV for the Higgs boson mass. The original motivation to use the recoil technique for a Higgs boson mass measurement independent on its decay modes could not be completely confirmed. For a Higgs boson mass of 180 GeV and 350 GeV, a statistics corresponding to 50/fb is not sufficient to achieve the necessary significance of the recoil mass peak above the background. The BeamCal is a calorimeter in the very forward region, about 3 m away from the nominal interaction point and surrounding the beam pipe. Due to its location, a lot of beamstrahlung pair particles will hit this calorimeter, representing a challenge for the operational reliability of the sensors under such harsh radiation conditions. We investigated single-crystal and polycrystalline CVD diamond, gallium arsenide and radiation-hard silicon as sensor candidates for their radiation hardness and found that diamond and gallium arsenide are promising. We used a 10 MeV electron beam of few nA to irradiate the samples under investigation up to doses of 5 MGy for diamond, up to about 1.5 MGy for gallium arsenide and up to about 90 kGy for silicon. We measured in regular periods the CCD to characterize the impact of the absorbed dose on the size of the signal, which is generated by electrons of a Sr-90 source crossing the sensor. Additional measurements such as the dark current and the CCD as functions of the voltage completed the characterization of the sensor candidates. For the single-crystal CVD diamond, also the thermally stimulated current was measured to determine amongst others the defect density created by irradiation. In the diamond samples, evidence for strong polarization effects inside the material was found and investigated in more detail. A phenomenological model based on semi-conductor physics was developed to describe the sensor properties as a function of the applied electric field, the dose and the dose rate. Its predictions were compared with the results of the measurements. Several parameters such as time scales and cross-sections were determined using this model, which led to ongoing investigations.}, subject = {Detektor; Speicherring; Higgs-Teilchen; Higgs-Bosonmasse; Detektor; Detektorentwicklung; ILC; Higgs boson mass; Detector development; ILC}, language = {en} } @book{Martin2009, author = {Martin,}, title = {Le philosophe Pyrrhonien : com{\´e}die en trois actes ; texte {\´e}tabli d'apr{\`e}s l'{\´e}dition d'Angers, 1761}, editor = {Kuhn, Karl-Heinz}, doi = {10.26127/BTUOpen-6254}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus4-62544}, publisher = {BTU Cottbus - Senftenberg}, year = {2009}, abstract = {La com{\´e}die "Le Philosophe Pyrrhonien" a {\´e}t{\´e} publi{\´e}e en 1761 {\`a} Angers, dans le nord de la France. L'auteur de l'oeuvre est Monsieur Martin, professeur au coll{\`e}ge de Ch{\^a}teau-Gontier. Avec sa pi{\`e}ce de th{\´e}{\^a}tre, Martin veut r{\´e}futer le scepticisme du philosophe grec Pyrrhon (~360 - ~270 av. J.-C.) et faire conna{\^i}tre {\`a} son public la th{\´e}orie de la connaissance et l'{\´e}thique d'Aristote. L'ouvrage, publi{\´e} {\`a} l'apog{\´e}e des Lumi{\`e}res, est donc aussi -sous une forme voil{\´e}e- un t{\´e}moignage des d{\´e}bats philosophiques de son {\´e}poque.}, subject = {Th{\´e}{\^a}tre; French; Franz{\"o}sisch; France; 18e si{\`e}cle; 1761; Aristotelisme; Scepticisme; Comedy; History 1761; Scepticism; Pyrrhonism; Stage play; Kom{\"o}die; Geschichte 1761; Skeptizismus; Pyrrhonismus; Theaterst{\"u}ck}, language = {fr} } @phdthesis{Strehler2011, author = {Strehler, Martin}, title = {Signalized flows - optimizing traffic signals and guideposts and related network flow problems}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus-23637}, school = {BTU Cottbus - Senftenberg}, year = {2011}, abstract = {Guideposts and traffic signals are important devices for controlling inner-city traffic and their optimized operation is essential for efficient traffic flow without congestion. In this thesis, we develop a mathematical model for guideposts and traffic signals in the context of network flow theory. Guideposts lead to confluent flows where each node in the network may have at most one outgoing flow-carrying arc. The complexity of finding maximum confluent flows is studied and several polynomial time algorithms for special graph classes are developed. For traffic signal optimization, a cyclically time-expanded model is suggested which provides the possibility of the simultaneous optimization of offsets and traffic assignment. Thus, the influence of offsets on travel times can be accounted directly. The potential of the presented approach is demonstrated by simulation of real-world instances.}, subject = {Stadtverkehr; Verkehrsablauf; Netzwerkfluss; Optimierung; Netzwerkfluss; Verkehrsfluss; Konfluenter Fluss; Lichtsignalanlagenoptimierung; Optimierung von Wegweisern; Network flow; Traffic flow; Confluent flow; Traffic signal optimization; Flow with path restrictions}, language = {en} } @book{HaefnerLaschewskiColelletal.2013, author = {H{\"a}fner, Daniel and Laschewski, Lutz and Colell, Arwen and Groß, Steffen and Kosel, Heiko and Ramstedt, Martin and Rathgeber, Theodor}, title = {Die Rechte indigener V{\"o}lker an nat{\"u}rlichen Ressourcen und die Sorben/Wenden}, issn = {2198-4689}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus-29566}, publisher = {BTU Cottbus - Senftenberg}, year = {2013}, abstract = {In diesem Band sammeln wir Beitr{\"a}ge, die zum Anlass einer Tagung am 19.10.2013 an der BTU Cottbus - Senftenberg gehalten und f{\"u}r diese Ver{\"o}ffentlichung von den Referenten ausformuliert wurden. Im Zentrum der Tagung stand die internationale Konvention der ILO 169, welche Rechte indigener V{\"o}lker definiert, und die Frage, inwieweit diese Konvention und andere Ans{\"a}tze der (Selbst-)Organisation von Verf{\"u}gungsrechten an Natur Anregungen f{\"u}r die Ausgestaltung der Selbstverwaltungsrechte der Minderheit der Sorben/Wenden bieten.}, subject = {Sorben; Indigenes Volk; Nat{\"u}rliche Ressourcen; Kongress; Cottbus <2013>}, language = {de} } @phdthesis{Schwarick2013, author = {Schwarick, Martin}, title = {Symbolic on-the-fly analysis of stochastic Petri nets}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus4-30560}, school = {BTU Cottbus - Senftenberg}, year = {2013}, abstract = {This thesis investigates the efficient analysis, especially the model checking, of bounded stochastic Petri nets (SPNs) which can be augmented with reward structures. An SPN induces a continuous-time Markov chain (CTMC). A reward structure associates a reward to each state of the CTMC and defines a Markov reward model (MRM). The Continuous Stochastic Reward Logic (CSRL) permits to define sophisticated properties of CTMCs and MRMs which can be automatically verified by a model checker. CSRL model checking can be realized on top of established numerical analysis techniques for CTMCs which are based on the multiplication of a matrix and a vector. However, as these techniques consider a matrix and a vector at least in the size of the number of reachable states, it is still challenging to deal with the famous state space explosion problem. Several approaches, as for instance the use of Multi-terminal Decision Diagrams or Kronecker products to represent the matrix, have been investigated so far. They often enable the implementation of efficient CTMC analysis and are available in a couple of tools. As an alternative to these established techniques I enhance the idea of an on-the-fly computation of the matrix entries deploying a symbolic state space representation. The set of state transitions defining the matrix will be enumerated by the firing of the transitions of the given SPN for all reachable states. The reachable states are encoded by means of Interval Decision Diagrams (IDD). Further, I discuss crucial aspects for the implementation of the first multi-threaded symbolic CSRL model checker which is based on the developed technique and available in the tool MARCIE. An experimental comparison with the probabilistic model checker PRISM for a large number of experiments proves empirically the efficiency of the approach and its implementation, especially when investigating biological models.}, subject = {Stochastic Petri nets; Continuous-time Markov Chains; Model Checking; Interval Decision Diagrams; Continuous Stochastic Reward Logic; Stochastische Petrinetze; Zeit-kontinuierliche Markovketten; Intervalentscheidungsdiagramme; Modelchecking; Kontinuierliche Stochastiche Reward Logik; Stochstisches Petri-Netz; Markov-Kette; Programmverifikation}, language = {en} } @phdthesis{Hundt2015, author = {Hundt, Martin}, title = {Der AlkaPolP-Prozess als Ausgangspunkt f{\"u}r eine lignocellulosebasierte Bioraffinerie}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus4-35350}, school = {BTU Cottbus - Senftenberg}, year = {2015}, abstract = {Ausgehend von der bestehenden Idee eines Lignocelluloseaufschlusses in einem alkalischen Polyol (Alkaline Polyol Pulping = AlkaPolP) wurden im Rahmen dieser Arbeit ein Aufschlussprozess f{\"u}r Lignocellulosen in alkalischem Glycerin sowie die nachgeschaltete Aufbereitung der Produktstr{\"o}me entwickelt und gezeigt, dass diese den Ausgangspunkt eines vielversprechenden Bioraffineriekonzeptes bilden k{\"o}nnen. Es wurde nachgewiesen, dass der AlkaPolP-Prozess f{\"u}r alle Arten von Lignocellulose geeignet ist und diese innerhalb weniger Minuten nahezu vollst{\"a}ndig delignifiziert. Im Rahmen des Downstream Processings der Aufschlussprodukte wurden die enzymatische Hydrolyse des Zellstoffes, die Ligninf{\"a}llung sowie die Aufreinigung des Ligninfiltrates genauer untersucht. Ein Vergleich mit Literaturdaten anderer Verfahren zur Lignocellulosefraktionierung zeigte, dass mit dem AlkaPolP-Prozess mindestens {\"a}hnliche Produktausbeuten und -qualit{\"a}ten erreicht werden. Vor allem f{\"u}r den Aufschluss von widerstandsf{\"a}higem Nadelholz ist der AlkaPolP-Prozess den meisten anderen Verfahren deutlich {\"u}berlegen. Nach der Konstruktion und Fertigung eines Reaktionsextruders wurden Betriebsbedingungen gefunden, mit denen Nadelholzschnitzel {\"u}ber mehrere Stunden hinweg in einem stabilen kontinuierlichen Prozess effektiv in alkalischem Glycerin aufgeschlossen werden konnten. Auf der Grundlage von Literaturdaten und der durchgef{\"u}hrten Experimente wurde ein Gesamtprozess entworfen, der neben bereits untersuchten Verfahrensstufen auch eine Aufarbeitung des Ligninfiltrates durch eine Elektrodialyse und mehrere Destillationsschritte umfasst und eine Regeneration der Einsatzstoffe sowie eine Abtrennung der w{\"a}hrend des Aufschlusses gebildeten Carbons{\"a}uren erm{\"o}glicht. Die Ergebnisse dieser Arbeit bilden den Grundstein f{\"u}r die Weiterentwicklung des AlkaPolP-Prozesses. Es konnte gezeigt werden, dass dieser, im kontinuierlichen Betrieb durchf{\"u}hrbare und f{\"u}r alle Arten von Lignocellulose geeignete, Aufschlussprozess einen vielversprechenden Ausgangspunkt f{\"u}r ein nachhaltiges Bioraffineriekonzept darstellt.}, subject = {Lignocellulose; AlkaPolP; Lignin; Bioraffinerie; Biorefinery; Lignocellulose; Polyole; Aufschluss ; Lignin; Bioraffinerie}, language = {de} } @techreport{SchwarickRohrHeiner2016, author = {Schwarick, Martin and Rohr, Christian and Heiner, Monika}, title = {MARCIE manual}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus4-40568}, year = {2016}, abstract = {This manual gives an overview on MARCIE - Model Checking And Reachability analysis done effiCIEntly. MARCIE was originally developed as a symbolic model checker for stochastic Petri nets, building on its predecessor - IDDMC - Interval Decision Diagram based Model Checking - which has been previously developed for the qualitative analysis of bounded Place/Transition nets extended by special arcs. Over the last years the tool has been enriched to allow also quantitative analysis of extended stochastic Petri nets. We concentrate here on the user viewpoint. For a detailed introduction to the relevant formalisms, formal definitions and algorithms we refer to related literature.}, subject = {Petri nets; Model checking; Model Checking; Petri-Netz}, language = {en} }