We provide a Kripke semantics for a STIT logic with the "next" operator. As the atemporal group STIT is undecidable and unaxiomatizable, we are interested in strict fragments of atemporal group STIT. First we prove that the satisfiability problem of a formula of the fragment made up of individual coalitions plus the grand coalition is also NEXPTIME-complete. We then generalize this result to a fragment where coalitions are in a given lattice. We also prove that if we restrict the language (...) to nested coalitions the satisfiability problem is NP-complete if the number of agents is fixed and PSPACE-complete if the number of agents is variable. Finally we embed individual STIT with the "next" operator into a fragment of atemporal group STIT. (shrink)

In this article, we present a modal logic that extends the basic modal logic with two dynamic operators: copy ( ), which replicates the current model, labelling each copy with a different propositional symbol and respecting accessibility relations even between distinct copies; and remove ( ), which deletes paths in the model that satisfy certain intermediate conditions. We call the resulting logic. We study its computational complexity, and its relative expressivity with respect to (static) modal logics and, and the dynamic (...) epistemic Action Model Logic,. (shrink)

In this article, we present a modal logic that extends the basic modal logic ML with two dynamic operators: copy, which replicates the current model, labelling each copy with a different prop...

This paper describes methods for generating interactive Euler diagrams. User interaction is needed to improve the aesthetic quality of the drawing without writing tedious formal specifications. More precisely, the user can modify the diagram’s layout on the fly by mouse control. We prove that the satisfiability problem is in \ and we provide two syntactic fragments such that the corresponding restricted satisfiability problem is already \-hard. We describe an improved local search based approach, a method inspired from the gradient method (...) and a hybrid method mixing both and. A software tool was implemented and its implementation is described. We also experimentally compare the different methods. We first see that the improved local search and the hybrid method outperforms the local search from the literature and the gradient method for generating a diagram. Concerning interaction, the local search approach is not suitable but hybrid method and gradient method give both good results in terms of quality of drawings and stability. Specifications are written using region connection calculus ), radius constraints and disjunctions. Euler diagrams are described as set of circles. (shrink)