Verifying Normative System Specification containing Collective Imperatives and Deadlines

Luca Gasparini; Timothy J. Norman; Martin J. Kollingbaum; Liang Chen; John-Jules Ch. Meyer

doi:10.5555/2772879.2773454

Verifying Normative System Specification containing Collective Imperatives and Deadlines

Luca Gasparini, Timothy J. Norman, Martin J. Kollingbaum, Liang Chen, John-Jules Ch. Meyer

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

Abstract

Our focus is on the specification and verification of normative systems that include contrary-to-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 model checker, we show how Linear Temporal Logic properties can be verified, and provide some experimental results.

Original language	English
Title of host publication	Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4-8, 2015
Editors	R. Bordini, E. Elkind, G. Weiss, P. Yolum
Place of Publication	Richland
Publisher	International Foundation for Autonomous Agents and Multiagent Systems
Pages	1821-1822
Number of pages	2
ISBN (Print)	978-1-4503-3413-6
DOIs	https://doi.org/10.5555/2772879.2773454
Publication status	Published - 2015
Event	International Conference on Autonomous Agents and Multiagent Systems (AAMAS ’15) - Istanbul, Turkey Duration: 4 May 2015 → 8 May 2015

Conference

Conference	International Conference on Autonomous Agents and Multiagent Systems (AAMAS ’15)
Country/Territory	Turkey
City	Istanbul
Period	4/05/15 → 8/05/15

Keywords

Model Checking
Normative Systems
Collective Imperatives

Access to Document

10.5555/2772879.2773454

verifyingFinal published version, 424 KBLicence: Taverne

http://dl.acm.org/citation.cfm?id=2773454

Cite this

Gasparini, L., Norman, T. J., Kollingbaum, M. J., Chen, L., & Meyer, J.-J. C. (2015). Verifying Normative System Specification containing Collective Imperatives and Deadlines. In R. Bordini, E. Elkind, G. Weiss, & P. Yolum (Eds.), Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4-8, 2015 (pp. 1821-1822). International Foundation for Autonomous Agents and Multiagent Systems. https://doi.org/10.5555/2772879.2773454

Gasparini, Luca ; Norman, Timothy J. ; Kollingbaum, Martin J. et al. / Verifying Normative System Specification containing Collective Imperatives and Deadlines. Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4-8, 2015. editor / R. Bordini ; E. Elkind ; G. Weiss ; P. Yolum. Richland : International Foundation for Autonomous Agents and Multiagent Systems, 2015. pp. 1821-1822

@inproceedings{3f1eb58dc5994007a9cd1c5cb85dff06,

title = "Verifying Normative System Specification containing Collective Imperatives and Deadlines",

abstract = "Our focus is on the specification and verification of normative systems that include contrary-to-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 model checker, we show how Linear Temporal Logic properties can be verified, and provide some experimental results.",

keywords = "Model Checking, Normative Systems, Collective Imperatives",

author = "Luca Gasparini and Norman, {Timothy J.} and Kollingbaum, {Martin J.} and Liang Chen and Meyer, {John-Jules Ch.}",

year = "2015",

doi = "10.5555/2772879.2773454",

language = "English",

isbn = "978-1-4503-3413-6",

pages = "1821--1822",

editor = "R. Bordini and E. Elkind and G. Weiss and P. Yolum",

booktitle = "Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4-8, 2015",

publisher = "International Foundation for Autonomous Agents and Multiagent Systems",

note = "International Conference on Autonomous Agents and Multiagent Systems (AAMAS {\textquoteright}15) ; Conference date: 04-05-2015 Through 08-05-2015",

}

Gasparini, L, Norman, TJ, Kollingbaum, MJ, Chen, L & Meyer, J-JC 2015, Verifying Normative System Specification containing Collective Imperatives and Deadlines. in R Bordini, E Elkind, G Weiss & P Yolum (eds), Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4-8, 2015. International Foundation for Autonomous Agents and Multiagent Systems, Richland, pp. 1821-1822, International Conference on Autonomous Agents and Multiagent Systems (AAMAS ’15) , Istanbul, Turkey, 4/05/15. https://doi.org/10.5555/2772879.2773454

Verifying Normative System Specification containing Collective Imperatives and Deadlines. / Gasparini, Luca; Norman, Timothy J.; Kollingbaum, Martin J. et al.
Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4-8, 2015. ed. / R. Bordini; E. Elkind; G. Weiss; P. Yolum. Richland: International Foundation for Autonomous Agents and Multiagent Systems, 2015. p. 1821-1822.

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

TY - GEN

T1 - Verifying Normative System Specification containing Collective Imperatives and Deadlines

AU - Gasparini, Luca

AU - Norman, Timothy J.

AU - Kollingbaum, Martin J.

AU - Chen, Liang

AU - Meyer, John-Jules Ch.

PY - 2015

Y1 - 2015

N2 - Our focus is on the specification and verification of normative systems that include contrary-to-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 model checker, we show how Linear Temporal Logic properties can be verified, and provide some experimental results.

AB - Our focus is on the specification and verification of normative systems that include contrary-to-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 model checker, we show how Linear Temporal Logic properties can be verified, and provide some experimental results.

KW - Model Checking

KW - Normative Systems

KW - Collective Imperatives

U2 - 10.5555/2772879.2773454

DO - 10.5555/2772879.2773454

M3 - Conference contribution

SN - 978-1-4503-3413-6

SP - 1821

EP - 1822

BT - Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4-8, 2015

A2 - Bordini, R.

A2 - Elkind, E.

A2 - Weiss, G.

A2 - Yolum, P.

PB - International Foundation for Autonomous Agents and Multiagent Systems

CY - Richland

T2 - International Conference on Autonomous Agents and Multiagent Systems (AAMAS ’15)

Y2 - 4 May 2015 through 8 May 2015

ER -

Gasparini L, Norman TJ, Kollingbaum MJ, Chen L, Meyer JJC. Verifying Normative System Specification containing Collective Imperatives and Deadlines. In Bordini R, Elkind E, Weiss G, Yolum P, editors, Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4-8, 2015. Richland: International Foundation for Autonomous Agents and Multiagent Systems. 2015. p. 1821-1822 doi: 10.5555/2772879.2773454

Verifying Normative System Specification containing Collective Imperatives and Deadlines

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this