Deciding extended modal logics by combining state space generation and SAT solving

This paper presents a method of deciding extended modal formulas that arise, in particular, when reasoning about transformations of relational structures and graphs. The method proceeds by first unwinding a structure that is an over-approximation of potential models, and then selecting effective models with the aid of a SAT solver.
 

Online Copy

• Conference version

BibTeX Entry

@inproceedings{strecker18:_decid_exten_modal_logic_combin,
  author    = {Martin Strecker},
  title     = {Deciding Extended Modal Logics by Combining State Space Generation
               and {SAT} Solving},
  booktitle = {Artificial Intelligence and Symbolic Computation - 13th International
               Conference, {AISC} 2018, Suzhou, China, September 16-19, 2018, Proceedings},
  editor    = {Jacques D. Fleuriot and
               Dongming Wang and
               Jacques Calmet},
  pages     = {119--135},
  year      = 2018,
  doi       = {10.1007/978-3-319-99957-9_8},
  series    = {Lecture Notes in Computer Science},
  volume    = {11110},
  publisher = {Springer},
  url       = {http://www.irit.fr/~Martin.Strecker/Publications/aisc2018.html}
}