An extension of QPTL is considered where functional dependencies among the quantified variables can be restricted in such a way that their current values are independent of the future values of the other variables . This restriction is tightly connected to the notion of behavioral strategies in game-theory and allows the resulting logic to naturally express game theoretic concepts . The extension is called behavioral quantifications and can be decided, for both model checking and satisfaction, in 2ExpTime .

Author(s) : Dylan Bellier, Massimo Benerecetti, Dario Della Monica, Fabio Mogavero

Links : PDF - Abstract

Code :

Keywords : game - variables - extension - behavioral - values -

Leave a Reply

Your email address will not be published. Required fields are marked *