Synthesis is the automated construction of a system from its specification. The system has to satisfy its specification in all possible environments. Modern systems often interact with other systems, or agents. Many times these agents have objectives of their own, other than to fail the system. Thus, it makes sense to model system environments not as hostile, but as composed of rational agents; i.e., agents that act to achieve their own objectives. We introduce the problem of synthesis in the context of rational agents (rational synthesis, for short). The input consists of a temporal-logic formula specifying the system and temporal-logic formulas specifying the objectives of the agents. The output is an implementation T of the system and a profile of strategies, suggesting a behavior for each of the agents. The output should satisfy two conditions. First, the composition of T with the strategy profile should satisfy the specification. Second, the strategy profile should be an equilibria in the sense that, in view of their objectives, agents have no incentive to deviate from the strategies assigned to them. We solve the rational-synthesis problem for various definitions of equilibria studied in game theory.
This is a joint work with Orna Kupferman and Yoad Lustig.
Dana Fisman has been working in the area of formal verification for over a decade. She did her MSc and PhD in this field under the supervision of Prof. Amir Pnueli at the Weizmann Institute of Science, Rehovot, Israel, and a postdoc at Prof. Orna Kupferman’s group at the Hebrew University, Jerusalem, Israel.
She has been working in the formal methods group of IBM Haifa Research Lab, and in the formal verification group of Synopsys Inc.
She has been an active participant in the Accellera and IEEE working groups working on the formulation of the IEEE-1850 standard for Property Specification Language (PSL). She co-authored the book "A Practical Introduction to PSL” Springer, 2006.