Algebraic derivation of Until rules and application to timer verification

Ertel, Jessica und Glück, Roland und möller, bernhard (2018) Algebraic derivation of Until rules and application to timer verification. In: LECTURE NOTES IN COMPUTER SCIENCE, 11194, Seiten 244-262. Springer. 17th International Conference on Relational and Algebraic Methods in Computer Science, 2018-10-29 - 2018-11-01, Groningen, Niederlande. doi: 10.1007/978-3-030-02149-8_15.

Dieses Archiv kann nicht den Volltext zur Verfügung stellen.

Offizielle URL: https://link.springer.com/chapter/10.1007/978-3-030-02149-8_15

Kurzfassung

Using correspondences between linear temporal logic and modal Kleene Algebra, we prove in an algebraic manner rules of linear temporal logic involving the until operator. These can be used to verify programmable logic controllers; as a case study we use a part of the control of pedestrian lights, verified with the interactive tool KIV.

elib-URL des Eintrags:

https://elib.dlr.de/122742/

Dokumentart:

Konferenzbeitrag (Vortrag)

Titel:

Algebraic derivation of Until rules and application to timer verification

Autoren:

Autoren	Institution oder E-Mail-Adresse	Autoren-ORCID-iD	ORCID Put Code
Ertel, Jessica	ertel-jessica (at) hotmail.de	NICHT SPEZIFIZIERT	NICHT SPEZIFIZIERT
Glück, Roland	roland.glueck (at) dlr.de	https://orcid.org/0000-0001-7909-1942	NICHT SPEZIFIZIERT
möller, bernhard	bernhard.moeller (at) informatik.uni-augsburg.de	NICHT SPEZIFIZIERT	NICHT SPEZIFIZIERT

Datum:

2018

Erschienen in:

LECTURE NOTES IN COMPUTER SCIENCE

Referierte Publikation:

Open Access:

Nein

Gold Open Access:

Nein

In SCOPUS:

Nein

In ISI Web of Science:

Band:

11194

DOI:

10.1007/978-3-030-02149-8_15

Seitenbereich:

Seiten 244-262

Herausgeber:

Herausgeber	Institution und/oder E-Mail-Adresse der Herausgeber	Herausgeber-ORCID-iD	ORCID Put Code
Desharnais, Jules	Jules.Desharnais (at) ift.ulaval.ca	NICHT SPEZIFIZIERT	NICHT SPEZIFIZIERT
Guttmann, Walter	walter.guttmann (at) canterbury.ac.nz	NICHT SPEZIFIZIERT	NICHT SPEZIFIZIERT
Joosten, Stef	stef. joosten (at) ou. nl	NICHT SPEZIFIZIERT	NICHT SPEZIFIZIERT

Verlag:

Springer

Name der Reihe:

Lecture Notes in Computer Science

Status:

veröffentlicht

Stichwörter:

PLC Verification Kleene Algebra Timer

Veranstaltungstitel:

17th International Conference on Relational and Algebraic Methods in Computer Science

Veranstaltungsort:

Groningen, Niederlande

Veranstaltungsart:

internationale Konferenz

Veranstaltungsbeginn:

29 Oktober 2018

Veranstaltungsende:

1 November 2018

HGF - Forschungsbereich:

Luftfahrt, Raumfahrt und Verkehr

HGF - Programm:

Luftfahrt

HGF - Programmthema:

keine Zuordnung

DLR - Schwerpunkt:

Luftfahrt

DLR - Forschungsgebiet:

L - keine Zuordnung

DLR - Teilgebiet (Projekt, Vorhaben):

L - keine Zuordnung

Standort:

Augsburg

Institute & Einrichtungen:

Institut für Bauweisen und Strukturtechnologie > Automation und Produktionstechnologie

Hinterlegt von:

Glück, Dr. Roland

Hinterlegt am:

15 Nov 2018 10:11

Letzte Änderung:

24 Apr 2024 20:26

Nur für Mitarbeiter des Archivs: Kontrollseite des Eintrags