Operational and logical semantics for polling real-time systems

P.R. Anders (Editor), Henning Dierks, Ansgar Fehnker, H. Rischel (Editor), Ansgar Fehnker, Angelika H. Mader, Frits Vaandrager

    • 12 Citations

    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 languageUndefined
    Pages29-40
    Number of pages12
    DOIs
    StatePublished - Sep 1998

    Fingerprint

    Semantics
    Programmable logic controllers
    Real time systems
    Hardware

    Keywords

    • IR-56216
    • EWI-1051

    Cite this

    Anders, P. R. (Ed.), Dierks, H., Fehnker, A., Rischel, H. (Ed.), Fehnker, A., Mader, A. H., & Vaandrager, F. (1998). Operational and logical semantics for polling real-time systems. 29-40. DOI: 10.1007/BFb0055334

    Anders, P.R. (Editor); Dierks, Henning; Fehnker, Ansgar; Rischel, H. (Editor); Fehnker, Ansgar; Mader, Angelika H.; Vaandrager, Frits / Operational and logical semantics for polling real-time systems.

    1998. 29-40.

    Research output: Scientific - peer-reviewPaper

    @misc{4fde28c8ab4147079e2dd96c261f3ba9,
    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.",
    keywords = "IR-56216, EWI-1051",
    author = "P.R. Anders and Henning Dierks and Ansgar Fehnker and H. Rischel and Ansgar Fehnker and Mader, {Angelika H.} and Frits Vaandrager",
    note = "Imported from DIES",
    year = "1998",
    month = "9",
    doi = "10.1007/BFb0055334",
    pages = "29--40",

    }

    Anders, PR (ed.), Dierks, H, Fehnker, A, Rischel, H (ed.), Fehnker, A, Mader, AH & Vaandrager, F 1998, 'Operational and logical semantics for polling real-time systems' pp. 29-40. DOI: 10.1007/BFb0055334

    Operational and logical semantics for polling real-time systems. / Anders, P.R. (Editor); Dierks, Henning; Fehnker, Ansgar; Rischel, H. (Editor); Fehnker, Ansgar; Mader, Angelika H.; Vaandrager, Frits.

    1998. 29-40.

    Research output: Scientific - peer-reviewPaper

    TY - CONF

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

    AU - Dierks,Henning

    AU - Fehnker,Ansgar

    AU - Fehnker,Ansgar

    AU - Mader,Angelika H.

    AU - Vaandrager,Frits

    A2 - Anders,P.R.

    A2 - Rischel,H.

    N1 - Imported from DIES

    PY - 1998/9

    Y1 - 1998/9

    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.

    KW - IR-56216

    KW - EWI-1051

    U2 - 10.1007/BFb0055334

    DO - 10.1007/BFb0055334

    M3 - Paper

    SP - 29

    EP - 40

    ER -

    Anders PR, (ed.), Dierks H, Fehnker A, Rischel H, (ed.), Fehnker A, Mader AH et al. Operational and logical semantics for polling real-time systems. 1998. Available from, DOI: 10.1007/BFb0055334