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