Spezifikation reaktiver Systeme durch temporal stratifizierte Programme
- Temporal stratifizierte Programme sind spezielle Logik-Programme auf der Grundlage einer linearen, temporalen Aussagenlogik, mit denen zustandsendliche reaktive Systeme spezifiziert werden können. Dabei wird die Umgebung eines zu implementierenden Steuerungsprogrammes durch eine Menge von PROLOG-ähnlichen Programmklauseln beschrieben; zusätzlich wird eine Sicherheitsbedingung angegeben, die in dem System gelten soll. Die Sprache ist so gestaltet, daß sie für resolutionsbasierte Verfahren zur Verifikation und Synthese von Steuerungsprogrammen geeignet ist. Wir zeigen, daß temporal stratifizierte Programme in ihrer Ausdrucksmächtigkeit endlichen Automaten gleichkommen.
Author: | Robi Malik, Otto Mayer |
---|---|
URN: | urn:nbn:de:hbz:386-kluedo-49897 |
Series (Serial Number): | Interner Bericht des Fachbereich Informatik (259) |
Document Type: | Report |
Language of publication: | German |
Date of Publication (online): | 2017/10/30 |
Year of first Publication: | 1994 |
Publishing Institution: | Technische Universität Kaiserslautern |
Date of the Publication (Server): | 2017/10/30 |
Page Number: | 26 |
Faculties / Organisational entities: | Kaiserslautern - Fachbereich Informatik |
DDC-Cassification: | 0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik |
Licence (German): | Creative Commons 4.0 - Namensnennung, nicht kommerziell, keine Bearbeitung (CC BY-NC-ND 4.0) |