Formal methods for checking realizability of coalitions in 3-party systems

Author

Banerjee, Ansuman ; Dasgupta, Pallab ; Chakrabarti, P.P.

Author_Institution

Dept. of Comput. Sci. & Eng., Indian Inst. of Technol., Kharagpur

fYear

2006

fDate

27-30 July 2006

Firstpage

198

Lastpage

198

Abstract

The main contributions of this paper are as follows: We revisit the concept of multiplayer coalition games in the context of a 3-party system. We analyze the coalition realizability problem for different degrees of observability of the module and the controller. We show that the realizability problem can be expressed as an instance of quantified Boolean formulas (QBF), by using appropriate quantifications on the variables of the environment, the module and the controller. We then use recent QBF solvers to verify

Keywords

Boolean functions; formal specification; formal verification; observability; realisation theory; coalition realizability problem; formal methods; multiplayer coalition games; observability; quantified Boolean formula; realizability checking; three-party systems; Application software; Computer science; Control systems; Electronic design automation and methodology; Instruments; Medical control systems; Microprocessors; Observability; Power engineering and energy; Switching circuits;

fLanguage

English

Publisher

ieee

Conference_Titel

Formal Methods and Models for Co-Design, 2006. MEMOCODE '06. Proceedings. Fourth ACM and IEEE International Conference on

Conference_Location

Napa, CA

Print_ISBN

1-4244-0421-5

Type

conf

DOI

10.1109/MEMCOD.2006.1695927

Filename

1695927