Operational and logical semantics for polling real-time systems

Henning Dierks; Ansgar Fehnker; Angelika Mader; Frits Vaandrager

doi:10.1007/BFb0055334

Operational and logical semantics for polling real-time systems

Henning Dierks, Ansgar Fehnker, Angelika Mader, Frits Vaandrager

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

12 Citations (Scopus)

Abstract

PLC-Automata are a class of real-time automata suitable to describe the behavior of polling real-time systems. PLC-Automata can be compiled to source code for PLCs, a hardware widely used in industry to control processes. Also, PLC-Automata have been equipped with a logical and operational semantics, using Duration Calculus (DC) and Timed Automata (TA), respectively.

The three main results of this paper are: (1) A simplified operational semantics. (2) A minor extension of the logical semantics, and a proof that this semantics is complete relative to our operational semantics. This means that if an observable satisfies all formulas of the DC semantics, then it can also be generated by the TA semantics. (3) A proof that the logical semantics is sound relative to our operational semantics. This means that each observable that is accepted by the TA semantics constitutes a model for all formulas of the DC semantics

Original language	English
Title of host publication	Formal Techniques in Real-Time and Fault-Tolerant Systems
Subtitle of host publication	5th International Symposium, FTRTFT'98 Lyngby, Denmark, September 14-18, 1998, Proceedings
Editors	Anders P. Ravn, Hans Rischel
Place of Publication	Berlin
Publisher	Springer, Springer Nature
Pages	29-40
Number of pages	12
ISBN (Print)	9783540650034, 3540650032
DOIs	https://doi.org/10.1007/BFb0055334
Publication status	Published - 1998
Externally published	Yes
Event	5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant System, FTRTFT 1998 - Lyngby, Denmark Duration: 14 Sept 1998 → 18 Sept 1998

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	1486
ISSN (Print)	0302-9743

Conference

Conference	5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant System, FTRTFT 1998
Abbreviated title	FTRTFT '98
Country/Territory	Denmark
City	Lyngby
Period	14/09/98 → 18/09/98

Access to Document

10.1007/BFb0055334

Cite this

Dierks, H., Fehnker, A., Mader, A., & Vaandrager, F. (1998). Operational and logical semantics for polling real-time systems. In A. P. Ravn, & H. Rischel (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems: 5th International Symposium, FTRTFT'98 Lyngby, Denmark, September 14-18, 1998, Proceedings (pp. 29-40). (Lecture Notes in Computer Science; Vol. 1486). Springer, Springer Nature. https://doi.org/10.1007/BFb0055334

Dierks, Henning ; Fehnker, Ansgar ; Mader, Angelika et al. / Operational and logical semantics for polling real-time systems. Formal Techniques in Real-Time and Fault-Tolerant Systems: 5th International Symposium, FTRTFT'98 Lyngby, Denmark, September 14-18, 1998, Proceedings. editor / Anders P. Ravn ; Hans Rischel. Berlin : Springer, Springer Nature, 1998. pp. 29-40 (Lecture Notes in Computer Science).

@inproceedings{9c107cafcb2848559e0e462feead03a1,

title = "Operational and logical semantics for polling real-time systems",

abstract = "PLC-Automata are a class of real-time automata suitable to describe the behavior of polling real-time systems. PLC-Automata can be compiled to source code for PLCs, a hardware widely used in industry to control processes. Also, PLC-Automata have been equipped with a logical and operational semantics, using Duration Calculus (DC) and Timed Automata (TA), respectively.The three main results of this paper are: (1) A simplified operational semantics. (2) A minor extension of the logical semantics, and a proof that this semantics is complete relative to our operational semantics. This means that if an observable satisfies all formulas of the DC semantics, then it can also be generated by the TA semantics. (3) A proof that the logical semantics is sound relative to our operational semantics. This means that each observable that is accepted by the TA semantics constitutes a model for all formulas of the DC semantics",

author = "Henning Dierks and Ansgar Fehnker and Angelika Mader and Frits Vaandrager",

year = "1998",

doi = "10.1007/BFb0055334",

language = "English",

isbn = "9783540650034",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Springer Nature",

pages = "29--40",

editor = "Ravn, {Anders P.} and Hans Rischel",

booktitle = "Formal Techniques in Real-Time and Fault-Tolerant Systems",

address = "United States",

note = "5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant System, FTRTFT 1998, FTRTFT '98 ; Conference date: 14-09-1998 Through 18-09-1998",

}

Dierks, H, Fehnker, A, Mader, A & Vaandrager, F 1998, Operational and logical semantics for polling real-time systems. in AP Ravn & H Rischel (eds), Formal Techniques in Real-Time and Fault-Tolerant Systems: 5th International Symposium, FTRTFT'98 Lyngby, Denmark, September 14-18, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1486, Springer, Springer Nature, Berlin, pp. 29-40, 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant System, FTRTFT 1998, Lyngby, Denmark, 14/09/98. https://doi.org/10.1007/BFb0055334

Operational and logical semantics for polling real-time systems. / Dierks, Henning; Fehnker, Ansgar; Mader, Angelika et al.
Formal Techniques in Real-Time and Fault-Tolerant Systems: 5th International Symposium, FTRTFT'98 Lyngby, Denmark, September 14-18, 1998, Proceedings. ed. / Anders P. Ravn; Hans Rischel. Berlin: Springer, Springer Nature, 1998. p. 29-40 (Lecture Notes in Computer Science; Vol. 1486).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Operational and logical semantics for polling real-time systems

AU - Dierks, Henning

AU - Fehnker, Ansgar

AU - Mader, Angelika

AU - Vaandrager, Frits

PY - 1998

Y1 - 1998

N2 - PLC-Automata are a class of real-time automata suitable to describe the behavior of polling real-time systems. PLC-Automata can be compiled to source code for PLCs, a hardware widely used in industry to control processes. Also, PLC-Automata have been equipped with a logical and operational semantics, using Duration Calculus (DC) and Timed Automata (TA), respectively.The three main results of this paper are: (1) A simplified operational semantics. (2) A minor extension of the logical semantics, and a proof that this semantics is complete relative to our operational semantics. This means that if an observable satisfies all formulas of the DC semantics, then it can also be generated by the TA semantics. (3) A proof that the logical semantics is sound relative to our operational semantics. This means that each observable that is accepted by the TA semantics constitutes a model for all formulas of the DC semantics

AB - PLC-Automata are a class of real-time automata suitable to describe the behavior of polling real-time systems. PLC-Automata can be compiled to source code for PLCs, a hardware widely used in industry to control processes. Also, PLC-Automata have been equipped with a logical and operational semantics, using Duration Calculus (DC) and Timed Automata (TA), respectively.The three main results of this paper are: (1) A simplified operational semantics. (2) A minor extension of the logical semantics, and a proof that this semantics is complete relative to our operational semantics. This means that if an observable satisfies all formulas of the DC semantics, then it can also be generated by the TA semantics. (3) A proof that the logical semantics is sound relative to our operational semantics. This means that each observable that is accepted by the TA semantics constitutes a model for all formulas of the DC semantics

U2 - 10.1007/BFb0055334

DO - 10.1007/BFb0055334

M3 - Conference proceeding contribution

SN - 9783540650034

SN - 3540650032

T3 - Lecture Notes in Computer Science

SP - 29

EP - 40

BT - Formal Techniques in Real-Time and Fault-Tolerant Systems

A2 - Ravn, Anders P.

A2 - Rischel, Hans

PB - Springer, Springer Nature

CY - Berlin

T2 - 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant System, FTRTFT 1998

Y2 - 14 September 1998 through 18 September 1998

ER -

Dierks H, Fehnker A, Mader A, Vaandrager F. Operational and logical semantics for polling real-time systems. In Ravn AP, Rischel H, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems: 5th International Symposium, FTRTFT'98 Lyngby, Denmark, September 14-18, 1998, Proceedings. Berlin: Springer, Springer Nature. 1998. p. 29-40. (Lecture Notes in Computer Science). doi: 10.1007/BFb0055334

Operational and logical semantics for polling real-time systems

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this