Validation task in COOL
As COOL started as an ontology reasoner it is natural to look at SHACL (a standard language for validating ontologies). The underlying logic itself (similar to PDL + grades + nominals) is maybe not that interesting for COOL however the validation task they use might be incorporated into COOL to make COOL usable for a range of new applications.
The validation task essentially takes a frame without valuation and a specification and checks whether a satisfying valuation can be found. Given that in the coalgebraic view, atoms can be seen as nullary modalities and hence part of the functor/world structure this task can be seen as simply leaving out part of the structure and trying to find a satisfying filler. This task conceptually lives somewhere in between model checking and satisfiability checking. When the completed model is constructed and returned there are different semantics to decide dependency loops in the specification and there are different semantics (e.g. well-founded or stable) similar to abstract argumentation semantics. See e.g. https://www.vldb.org/pvldb/vol15/p2284-ahmetaj.pdf
I see at least the following use cases that would be enabled by having such a generic implementation:
- AMCDES open model checking
- Abstract argumentation labelling semantics