Susmit Kumar Jha and Sanjit A. Seshia and Ashish Tiwari

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2011-16

March 4, 2011

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-16.pdf

Given a multi-modal dynamical system, optimal switching logic synthesis involves generating the conditions for switching between the system modes such that the resulting hybrid system satisfies a quantitative specification. We formalize and solve the problem of optimal switching logic synthesis for quantitative specifications over long run behavior. Each trajectory of the system, and each state of the system, is associated with a cost. Our goal is to synthesize a system that minimizes this cost from each initial state. Our paper generalizes earlier work on synthesis for safety as safety specifications can be encoded as quantitative specifications. We present an approach for specifying quantitative measures using reward and penalty functions, and illustrate its effectiveness using several examples. We present an automated technique to synthesize switching logic for such quantitative measures. Our algorithm is based on reducing the synthesis problem to an unconstrained numerical optimization problem which can be solved by any off-the-shelf numerical optimization engines. We demonstrate the effectiveness of this approach with experimental results.

---

BibTeX citation:

@techreport{Jha:EECS-2011-16,
    Author= {Jha, Susmit Kumar and Seshia, Sanjit A. and Tiwari, Ashish},
    Title= {Synthesizing Switching Logic to Minimize Long-Run Cost},
    Year= {2011},
    Month= {Mar},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-16.html},
    Number= {UCB/EECS-2011-16},
    Abstract= {Given a multi-modal dynamical system, optimal switching logic synthesis involves generating the conditions for switching between the system modes such that the resulting hybrid system satisfies a quantitative specification. We formalize and solve the problem of optimal switching logic synthesis for quantitative specifications over long run behavior. Each trajectory of the system, and each state of the system, is associated with a cost. Our goal is to synthesize a system that minimizes this cost from each initial state. Our paper generalizes earlier work on synthesis for safety as safety specifications can be encoded as quantitative specifications. We present an approach for specifying quantitative measures using reward and penalty functions, and illustrate its effectiveness using several examples. We present an automated technique to synthesize switching logic for such quantitative measures. Our algorithm is based on reducing the synthesis problem to an unconstrained numerical optimization problem which can be solved by any off-the-shelf numerical optimization engines. We demonstrate the effectiveness of this approach with experimental results.},
}

EndNote citation:

%0 Report
%A Jha, Susmit Kumar 
%A Seshia, Sanjit A. 
%A Tiwari, Ashish 
%T Synthesizing Switching Logic to Minimize Long-Run Cost
%I EECS Department, University of California, Berkeley
%D 2011
%8 March 4
%@ UCB/EECS-2011-16
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-16.html
%F Jha:EECS-2011-16