Verifying realizability and reachability in recursive interaction protocol specifications

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Verifying realizability and reachability in recursive interaction protocol specifications

Full text

Pdf (342 KB)

Source

International Conference on Autonomous Agents archive
Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems - Volume 2 table of contents

Budapest, Hungary

SESSION: Interactions table of contents

Pages 1233-1234

Year of Publication: 2009

ISBN:978-0-9817381-7-8

Authors

Hywel Dunn-Davies	Imperial College London, London, UK
Jim Cunningham	Imperial College London, London, UK

Sponsors

: The Foundation for Intelligent Physical Agents
Microsoft Research : Microsoft Research
: Whitestein Technologies
: European Office of Aerospace Research and Development, Air Force Office of Scientific Research, United States Air Force Research Laboratory
: Drexel University
: Wiley -- Blackwell Ltd

Publisher

International Foundation for Autonomous Agents and Multiagent Systems Richland, SC

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 14, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

ABSTRACT

The Propositional Statechart language described in [4] makes it possible to provide unambiguous joint diagrammatic specifications of complex recursive interaction protocols such as the multilateral voting protocol. Recursive protocols described using Propositional Statecharts are not necessarily finite state, meaning that verification of properties of these protocols cannot be achieved solely by means of finite state model checking. In this paper we discuss the verification of realizability, and reachability analysis, in recursive joint protocol specifications expressed using joint Propositional Statecharts.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Rajeev Alur , Michael Benedikt , Kousha Etessami , Patrice Godefroid , Thomas Reps , Mihalis Yannakakis, Analysis of recursive state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.4, p.786-818, July 2005 [doi>10.1145/1075382.1075387]
	2	Daniel Brand , Pitro Zafiropulo, On Communicating Finite-State Machines, Journal of the ACM (JACM), v.30 n.2, p.323-342, April 1983 [doi>10.1145/322374.322380]
	3	Desai, N. and Singh, M. P., Checking Enactability of Business Protocol Specifications, AAAI Conference on Artificial Intelligence (AAAI), 2008.
	4	Dunn-Davies, H. R., Cunningham, R. J. and Paurobally, S. Modularity and Composition in Propositonal Statecharts, In Proceedings of Diagrams 2006, LNCS 4045, Springer, 98--103, 2006.
	5	Hywel Dunn-Davies , Jim Cunningham, Deriving agent-centred representations of protocols described using propositional statecharts, Proceedings of the 6th international joint conference on Autonomous agents and multiagent systems, May 14-18, 2007, Honolulu, Hawaii [doi>10.1145/1329125.1329164]
	6	Fu, X., Bultan, T, and Su, J. Realizability of Conversation Protocols With Message Contents, International Journal of Web Services Research, 2(4), 68--93, 2005.