CÒIR

Verifying normative specifications of complex systems

Luca Gasparini*, Timothy J. Norman, Martin J. Kollingbaum, Liang Chen, John Jules C Meyer

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Existing approaches for the verification of normative systems consider limited representations of norms, often neglecting collective imperatives, deadlines and contrary-to-duty obligations. In order to capture the requirements of real-world scenarios, these structures are important. In this paper we propose methods for the specification and formal verification of complex normative systems that include contraryto- duty, collective and event-driven imperatives with deadlines. We propose an operational syntax and semantics for the specification of such systems. Using Maude and its linear temporal logic model checker, we show how important properties can be verified for such systems, and provide some experimental results for both bounded and unbounded verification.

Original languageEnglish
Title of host publicationCoordination, Organizations, Institutions, and Norms in Agent Systems XI
Subtitle of host publicationCOIN 2015 International Workshops, COIN@AAMAS, Istanbul, Turkey, May 4, 2015, COIN@IJCAI, Buenos Aires, Argentina, July 26, 2015, Revised Selected Papers
EditorsV Dignum, P Noriega, P Sensoy, J S Sichman
PublisherSpringer-Verlag
Pages134-153
Number of pages20
Volume9628
ISBN (Print)9783319426907
DOIs
Publication statusPublished - 2016
EventInternational Conference on Coordination, Organisations, Institutions and Norms in Agent Systems, 2015 - Istanbul, Turkey
Duration: 4 May 20154 May 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9628
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

ConferenceInternational Conference on Coordination, Organisations, Institutions and Norms in Agent Systems, 2015
CountryTurkey
CityIstanbul
Period4/05/154/05/15

Fingerprint

Large scale systems
Complex Systems
Deadline
Specification
Specifications
Temporal logic
Maude
Linear Temporal Logic
Event-driven
Semantics
Formal Verification
Norm
Scenarios
Requirements
Experimental Results
Model
Formal verification
Syntax

Keywords

  • Collective imperatives
  • Model checking
  • Normative systems

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Gasparini, L., Norman, T. J., Kollingbaum, M. J., Chen, L., & Meyer, J. J. C. (2016). CÒIR: Verifying normative specifications of complex systems. In V. Dignum, P. Noriega, P. Sensoy, & J. S. Sichman (Eds.), Coordination, Organizations, Institutions, and Norms in Agent Systems XI: COIN 2015 International Workshops, COIN@AAMAS, Istanbul, Turkey, May 4, 2015, COIN@IJCAI, Buenos Aires, Argentina, July 26, 2015, Revised Selected Papers (Vol. 9628, pp. 134-153). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9628). Springer-Verlag. https://doi.org/10.1007/978-3-319-42691-4_8

CÒIR : Verifying normative specifications of complex systems. / Gasparini, Luca; Norman, Timothy J.; Kollingbaum, Martin J.; Chen, Liang; Meyer, John Jules C.

Coordination, Organizations, Institutions, and Norms in Agent Systems XI: COIN 2015 International Workshops, COIN@AAMAS, Istanbul, Turkey, May 4, 2015, COIN@IJCAI, Buenos Aires, Argentina, July 26, 2015, Revised Selected Papers. ed. / V Dignum; P Noriega; P Sensoy; J S Sichman. Vol. 9628 Springer-Verlag, 2016. p. 134-153 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9628).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Gasparini, L, Norman, TJ, Kollingbaum, MJ, Chen, L & Meyer, JJC 2016, CÒIR: Verifying normative specifications of complex systems. in V Dignum, P Noriega, P Sensoy & JS Sichman (eds), Coordination, Organizations, Institutions, and Norms in Agent Systems XI: COIN 2015 International Workshops, COIN@AAMAS, Istanbul, Turkey, May 4, 2015, COIN@IJCAI, Buenos Aires, Argentina, July 26, 2015, Revised Selected Papers. vol. 9628, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9628, Springer-Verlag, pp. 134-153, International Conference on Coordination, Organisations, Institutions and Norms in Agent Systems, 2015, Istanbul, Turkey, 4/05/15. https://doi.org/10.1007/978-3-319-42691-4_8
Gasparini L, Norman TJ, Kollingbaum MJ, Chen L, Meyer JJC. CÒIR: Verifying normative specifications of complex systems. In Dignum V, Noriega P, Sensoy P, Sichman JS, editors, Coordination, Organizations, Institutions, and Norms in Agent Systems XI: COIN 2015 International Workshops, COIN@AAMAS, Istanbul, Turkey, May 4, 2015, COIN@IJCAI, Buenos Aires, Argentina, July 26, 2015, Revised Selected Papers. Vol. 9628. Springer-Verlag. 2016. p. 134-153. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-42691-4_8
Gasparini, Luca ; Norman, Timothy J. ; Kollingbaum, Martin J. ; Chen, Liang ; Meyer, John Jules C. / CÒIR : Verifying normative specifications of complex systems. Coordination, Organizations, Institutions, and Norms in Agent Systems XI: COIN 2015 International Workshops, COIN@AAMAS, Istanbul, Turkey, May 4, 2015, COIN@IJCAI, Buenos Aires, Argentina, July 26, 2015, Revised Selected Papers. editor / V Dignum ; P Noriega ; P Sensoy ; J S Sichman. Vol. 9628 Springer-Verlag, 2016. pp. 134-153 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{878b681cfa8f4655a90b916420499591,
title = "C{\`O}IR: Verifying normative specifications of complex systems",
abstract = "Existing approaches for the verification of normative systems consider limited representations of norms, often neglecting collective imperatives, deadlines and contrary-to-duty obligations. In order to capture the requirements of real-world scenarios, these structures are important. In this paper we propose methods for the specification and formal verification of complex normative systems that include contraryto- duty, collective and event-driven imperatives with deadlines. We propose an operational syntax and semantics for the specification of such systems. Using Maude and its linear temporal logic model checker, we show how important properties can be verified for such systems, and provide some experimental results for both bounded and unbounded verification.",
keywords = "Collective imperatives, Model checking, Normative systems",
author = "Luca Gasparini and Norman, {Timothy J.} and Kollingbaum, {Martin J.} and Liang Chen and Meyer, {John Jules C}",
year = "2016",
doi = "10.1007/978-3-319-42691-4_8",
language = "English",
isbn = "9783319426907",
volume = "9628",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "134--153",
editor = "V Dignum and P Noriega and P Sensoy and Sichman, {J S}",
booktitle = "Coordination, Organizations, Institutions, and Norms in Agent Systems XI",

}

TY - GEN

T1 - CÒIR

T2 - Verifying normative specifications of complex systems

AU - Gasparini, Luca

AU - Norman, Timothy J.

AU - Kollingbaum, Martin J.

AU - Chen, Liang

AU - Meyer, John Jules C

PY - 2016

Y1 - 2016

N2 - Existing approaches for the verification of normative systems consider limited representations of norms, often neglecting collective imperatives, deadlines and contrary-to-duty obligations. In order to capture the requirements of real-world scenarios, these structures are important. In this paper we propose methods for the specification and formal verification of complex normative systems that include contraryto- duty, collective and event-driven imperatives with deadlines. We propose an operational syntax and semantics for the specification of such systems. Using Maude and its linear temporal logic model checker, we show how important properties can be verified for such systems, and provide some experimental results for both bounded and unbounded verification.

AB - Existing approaches for the verification of normative systems consider limited representations of norms, often neglecting collective imperatives, deadlines and contrary-to-duty obligations. In order to capture the requirements of real-world scenarios, these structures are important. In this paper we propose methods for the specification and formal verification of complex normative systems that include contraryto- duty, collective and event-driven imperatives with deadlines. We propose an operational syntax and semantics for the specification of such systems. Using Maude and its linear temporal logic model checker, we show how important properties can be verified for such systems, and provide some experimental results for both bounded and unbounded verification.

KW - Collective imperatives

KW - Model checking

KW - Normative systems

UR - http://www.scopus.com/inward/record.url?scp=84978826701&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-42691-4_8

DO - 10.1007/978-3-319-42691-4_8

M3 - Conference contribution

SN - 9783319426907

VL - 9628

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 134

EP - 153

BT - Coordination, Organizations, Institutions, and Norms in Agent Systems XI

A2 - Dignum, V

A2 - Noriega, P

A2 - Sensoy, P

A2 - Sichman, J S

PB - Springer-Verlag

ER -