Steen Vester

Date: 16:00, Tuesday, September 23, 2014
Speaker: Steen Vester
Venue: IST Austria

 We consider model-checking of ATL and ATL* extended with counter constraints on one-counter game models (with VASS semantics). The combined complexity and data complexity of model-checking these logics are determined, both in the non-succinct and succinct case. In the non-succinct case only integer values in {-1,0,1} are allowed as counter updates whereas in the succinct case any integer weights, encoded in binary, are allowed.

Posted in RiSE Seminar