A logic for the specification of multi-object systems

Jan Broersen, Roelf J. Wieringa

Abstract

We present Multi-Object Dynamic Logic (MODL), a generalization of Dynamic Logic of which the intended use is the declarative specication of systems that are conceptually described by a multitude of objects. The semantics and entailment properties of MODL are based on some a priori requirements for a modal multi-object specication logic. In an example specication of the controls of a railroad crossing we demonstrate how MODL can be used to give semantics and reasoning capacity to graphical languages for communicating multi-object systems. In this example we introduce the idea of identifying the concept of event-triggering, which is used in the graphical languages, with the concept of action implication (action calling) in MODL. Finally we study to what extend temporal and mixed dynamic/temporal properties can be expressed in MODL.
Original languageUndefined
Title of host publicationThird International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS)
EditorsPaolo Ciancarini, Alessandro Fantechi, Robert Gorrieri
Place of PublicationDeventer, the Netherlands
PublisherKluwer Academic Publishers
Pages387-398
Number of pages12
ISBN (Print)0792384296
DOIs
StatePublished - Feb 1999

Publication series

NameIFIP Conference Proceedings
PublisherKluwer Academic Publishers
Volume139

Fingerprint

Railroad crossings
Semantics

Keywords

  • METIS-118903
  • SCS-Services
  • IR-64216
  • EWI-10570

Cite this

Broersen, J., & Wieringa, R. J. (1999). A logic for the specification of multi-object systems. In P. Ciancarini, A. Fantechi, & R. Gorrieri (Eds.), Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) (pp. 387-398). (IFIP Conference Proceedings; Vol. 139). Deventer, the Netherlands: Kluwer Academic Publishers. DOI: 10.1007/978-0-387-35562-7_30

Broersen, Jan; Wieringa, Roelf J. / A logic for the specification of multi-object systems.

Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS). ed. / Paolo Ciancarini; Alessandro Fantechi; Robert Gorrieri. Deventer, the Netherlands : Kluwer Academic Publishers, 1999. p. 387-398 (IFIP Conference Proceedings; Vol. 139).

Research output: Scientific - peer-reviewChapter

@inbook{966fb19e7f364dc1bc947a2c4b0ecc6a,
title = "A logic for the specification of multi-object systems",
abstract = "We present Multi-Object Dynamic Logic (MODL), a generalization of Dynamic Logic of which the intended use is the declarative specication of systems that are conceptually described by a multitude of objects. The semantics and entailment properties of MODL are based on some a priori requirements for a modal multi-object specication logic. In an example specication of the controls of a railroad crossing we demonstrate how MODL can be used to give semantics and reasoning capacity to graphical languages for communicating multi-object systems. In this example we introduce the idea of identifying the concept of event-triggering, which is used in the graphical languages, with the concept of action implication (action calling) in MODL. Finally we study to what extend temporal and mixed dynamic/temporal properties can be expressed in MODL.",
keywords = "METIS-118903, SCS-Services, IR-64216, EWI-10570",
author = "Jan Broersen and Wieringa, {Roelf J.}",
year = "1999",
month = "2",
doi = "10.1007/978-0-387-35562-7_30",
isbn = "0792384296",
series = "IFIP Conference Proceedings",
publisher = "Kluwer Academic Publishers",
pages = "387--398",
editor = "Paolo Ciancarini and Alessandro Fantechi and Robert Gorrieri",
booktitle = "Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS)",

}

Broersen, J & Wieringa, RJ 1999, A logic for the specification of multi-object systems. in P Ciancarini, A Fantechi & R Gorrieri (eds), Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS). IFIP Conference Proceedings, vol. 139, Kluwer Academic Publishers, Deventer, the Netherlands, pp. 387-398. DOI: 10.1007/978-0-387-35562-7_30

A logic for the specification of multi-object systems. / Broersen, Jan; Wieringa, Roelf J.

Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS). ed. / Paolo Ciancarini; Alessandro Fantechi; Robert Gorrieri. Deventer, the Netherlands : Kluwer Academic Publishers, 1999. p. 387-398 (IFIP Conference Proceedings; Vol. 139).

Research output: Scientific - peer-reviewChapter

TY - CHAP

T1 - A logic for the specification of multi-object systems

AU - Broersen,Jan

AU - Wieringa,Roelf J.

PY - 1999/2

Y1 - 1999/2

N2 - We present Multi-Object Dynamic Logic (MODL), a generalization of Dynamic Logic of which the intended use is the declarative specication of systems that are conceptually described by a multitude of objects. The semantics and entailment properties of MODL are based on some a priori requirements for a modal multi-object specication logic. In an example specication of the controls of a railroad crossing we demonstrate how MODL can be used to give semantics and reasoning capacity to graphical languages for communicating multi-object systems. In this example we introduce the idea of identifying the concept of event-triggering, which is used in the graphical languages, with the concept of action implication (action calling) in MODL. Finally we study to what extend temporal and mixed dynamic/temporal properties can be expressed in MODL.

AB - We present Multi-Object Dynamic Logic (MODL), a generalization of Dynamic Logic of which the intended use is the declarative specication of systems that are conceptually described by a multitude of objects. The semantics and entailment properties of MODL are based on some a priori requirements for a modal multi-object specication logic. In an example specication of the controls of a railroad crossing we demonstrate how MODL can be used to give semantics and reasoning capacity to graphical languages for communicating multi-object systems. In this example we introduce the idea of identifying the concept of event-triggering, which is used in the graphical languages, with the concept of action implication (action calling) in MODL. Finally we study to what extend temporal and mixed dynamic/temporal properties can be expressed in MODL.

KW - METIS-118903

KW - SCS-Services

KW - IR-64216

KW - EWI-10570

U2 - 10.1007/978-0-387-35562-7_30

DO - 10.1007/978-0-387-35562-7_30

M3 - Chapter

SN - 0792384296

T3 - IFIP Conference Proceedings

SP - 387

EP - 398

BT - Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS)

PB - Kluwer Academic Publishers

ER -

Broersen J, Wieringa RJ. A logic for the specification of multi-object systems. In Ciancarini P, Fantechi A, Gorrieri R, editors, Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS). Deventer, the Netherlands: Kluwer Academic Publishers. 1999. p. 387-398. (IFIP Conference Proceedings). Available from, DOI: 10.1007/978-0-387-35562-7_30