Coalgebraic Reasoning for Quantitative System Analysis

点击翻译按钮获取中文摘要

Modal logic serves as a formalism for the description of systems composed of nodes variously thought of as states, worlds, or individuals, and the interrelation between such nodes in a broad sense. It is widely applied in diverse contexts ranging from concurrency to knowledge representation. Quantitative modal logics deviate from the standard two-valued setup in that they take truth values in a domain that allows for degrees of truth in between complete truth and complete falsity. A typical example of such a domain of truth values is the real unit interval. Truth values in this domain may be read, for instance, as expressing vague qualifications, such as person being tall, in the vein of fuzzy logic. However, real-valuedness of truth arises also in other contexts, e.g. in probabilistic systems or in systems where states or transitions carry labels taken from a given metric space. More generally, truth domains that allow for measuring the deviation between truth values are usefully abstracted as so-called quantales. The object of CoRSA is to provide automated reasoning support for quantitative modal logics in this sense, aiming for genericity of reasoning algorithms over the system type (probabilistic, game-based, metric etc.) and over the semantics of the modalities, which in turn range from fuzzy relational modalities of the type `there is some successor / for all successors' over expectation-based probabilistic modalities of the type 'probably' to game-based modalities of the type a given coalition of agents can enforce some quantitative property'. To this end, we will work in the generic framework of universal coalgebra and, more specifically, coalgebraic logic, which provide categorical abstractions for the system type and the modalities. From work on reasoning in fuzzy description logics, it is known that the computational properties of quantitative modal logics depend rather strongly on which propositional connectives are included, up to the point that some reasoning problems become undecidable for certain propositional bases. Recent work on the connection between quantitative modal logics and notions of behavioral distance suggests that a point of balance between expressiveness and computational tractability may be found by focusing on non-expansive propositional operations, a point that we will clarify in the project. We thus expect to provide a generic framework for quantitative modal logics that stays close to semantic notions of behavioral distance and allows automated deduction in reasonable complexity.