A logic for the specification of multi-object systems

Jan Broersen; Roel Wieringa

doi:10.1007/978-0-387-35562-7_30

A logic for the specification of multi-object systems

Jan Broersen, Roel Wieringa

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

42 Downloads (Pure)

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 language	English
Title of host publication	Formal Methods for Open Object-Based Distributed Systems
Subtitle of host publication	IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS)
Editors	Paolo Ciancarini, Alessandro Fantechi, Robert Gorrieri
Place of Publication	Boston, MA
Publisher	Kluwer Academic Publishers
Pages	387-398
Number of pages	12
ISBN (Electronic)	978-0-387-35562-7
ISBN (Print)	978-1-4757-5266-3
DOIs	https://doi.org/10.1007/978-0-387-35562-7_30
Publication status	Published - Feb 1999
Event	3rd IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 1999 - Florence, Italy Duration: 15 Feb 1999 → 18 Feb 1999 Conference number: 3

Publication series

Name	IFIP Advances in Information and Communication Technology
Publisher	Kluwer Academic Publishers
Volume	10
ISSN (Print)	1868-4238
ISSN (Electronic)	1868-422X

Conference

Conference	3rd IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 1999
Abbreviated title	FMOODS
Country	Italy
City	Florence
Period	15/02/99 → 18/02/99

Keywords

SCS-Services
Dynamic logic
Liveness property
Action symbol
State predicate
Intuitive meaning

Access to Document

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

Broersen1999formal
open
Accepted author version, 219 KB

Fingerprint Dive into the research topics of 'A logic for the specification of multi-object systems'. Together they form a unique fingerprint.

Cite this

Broersen, J., & Wieringa, R. (1999). A logic for the specification of multi-object systems. In P. Ciancarini, A. Fantechi, & R. Gorrieri (Eds.), Formal Methods for Open Object-Based Distributed Systems: IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) (pp. 387-398). (IFIP Advances in Information and Communication Technology; Vol. 10). Kluwer Academic Publishers. https://doi.org/10.1007/978-0-387-35562-7_30

Broersen, Jan ; Wieringa, Roel. / A logic for the specification of multi-object systems. Formal Methods for Open Object-Based Distributed Systems: IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS). editor / Paolo Ciancarini ; Alessandro Fantechi ; Robert Gorrieri. Boston, MA : Kluwer Academic Publishers, 1999. pp. 387-398 (IFIP Advances in Information and Communication Technology).

@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 = "SCS-Services, Dynamic logic, Liveness property, Action symbol, State predicate, Intuitive meaning",

author = "Jan Broersen and Roel Wieringa",

year = "1999",

month = feb,

doi = "10.1007/978-0-387-35562-7_30",

language = "English",

isbn = "978-1-4757-5266-3",

series = "IFIP Advances in Information and Communication Technology",

publisher = "Kluwer Academic Publishers",

pages = "387--398",

editor = "Paolo Ciancarini and Alessandro Fantechi and Robert Gorrieri",

booktitle = "Formal Methods for Open Object-Based Distributed Systems",

address = "Netherlands",

note = "3rd IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 1999, FMOODS ; Conference date: 15-02-1999 Through 18-02-1999",

}

Broersen, J & Wieringa, R 1999, A logic for the specification of multi-object systems. in P Ciancarini, A Fantechi & R Gorrieri (eds), Formal Methods for Open Object-Based Distributed Systems: IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS). IFIP Advances in Information and Communication Technology, vol. 10, Kluwer Academic Publishers, Boston, MA, pp. 387-398, 3rd IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 1999, Florence, Italy, 15/02/99. https://doi.org/10.1007/978-0-387-35562-7_30

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

Formal Methods for Open Object-Based Distributed Systems: IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS). ed. / Paolo Ciancarini; Alessandro Fantechi; Robert Gorrieri. Boston, MA : Kluwer Academic Publishers, 1999. p. 387-398 (IFIP Advances in Information and Communication Technology; Vol. 10).

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

TY - CHAP

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

AU - Broersen, Jan

AU - Wieringa, Roel

N1 - Conference code: 3

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 - SCS-Services

KW - Dynamic logic

KW - Liveness property

KW - Action symbol

KW - State predicate

KW - Intuitive meaning

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

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

M3 - Chapter

SN - 978-1-4757-5266-3

T3 - IFIP Advances in Information and Communication Technology

SP - 387

EP - 398

BT - Formal Methods for Open Object-Based Distributed Systems

A2 - Ciancarini, Paolo

A2 - Fantechi, Alessandro

A2 - Gorrieri, Robert

PB - Kluwer Academic Publishers

CY - Boston, MA

T2 - 3rd IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 1999

Y2 - 15 February 1999 through 18 February 1999

ER -

Broersen J, Wieringa R. A logic for the specification of multi-object systems. In Ciancarini P, Fantechi A, Gorrieri R, editors, Formal Methods for Open Object-Based Distributed Systems: IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS). Boston, MA: Kluwer Academic Publishers. 1999. p. 387-398. (IFIP Advances in Information and Communication Technology). https://doi.org/10.1007/978-0-387-35562-7_30