New Remarks on the Concept in Logical Use

The main thesis of this paper is directed against the traditional (cognitivetheoretical) definition of the concept which claims that the concept is the '' thought about the essence of the object being thought'', i.e. that it is “a set of essential features or essential characteristics of an object''. But the '' set of essential features or essential characteristics of an object of thought'' is a '' content’’ of the thought. The thought about the essence of an object is definition and the concept is not definition but the part of definition! Besides as the part of formal structure of thought, the concept possesses calculative logical properties that in formal logic (be it syllogistics, or the logic of propositions, or the logic of predicates) come to the front place of formal logical computation. Without the calculative properties of the concept, there would be no calculative properties of propositions which express the thought (thought structures). The calculative properties of a concept include the (1) degree of its logical generality (degree of variability), the (2) logical relations it can establish within the whole of the conceptual content, the (3) operability of the concept in structure of affirmation and negation, the (4) deducibility of either axiomatic or probabilistic systems. Therefore, I believe that, from the logical point of view, the definition of a concept should be applied in favor of its calculative properties that it possesses.

Rational Verification for Probabilistic Systems

Rational verification is the problem of determining which temporal logic properties will hold in a multi-agent system, under the assumption that agents in the system act rationally, by choosing strategies that collectively form a game-theoretic equilibrium. Previous work in this area has largely focussed on deterministic systems. In this paper, we develop the theory and algorithms for rational verification in probabilistic systems. We focus on concurrent stochastic games (CSGs), which can be used to model uncertainty and randomness in complex multi-agent environments. We study the rational verification problem for both non-cooperative games and cooperative games in the qualitative probabilistic setting. In the former case, we consider LTL properties satisfied by the Nash equilibria of the game and in the latter case LTL properties satisfied by the core. In both cases, we show that the problem is 2EXPTIME-complete, thus not harder than the much simpler verification problem of model checking LTL properties of systems modelled as Markov decision processes (MDPs).

A Unifying Coalgebraic Semantics Framework for Quantum Systems

As a quantum counterpart of labeled transition system (LTS), quantum labeled transition system (QLTS) is a powerful formalism for modeling quantum programs or protocols, and gives a categorical understanding for quantum computation. With the help of quantum branching monad, QLTS provides a framework extending some ideas in non-deterministic or probabilistic systems to quantum systems. On the other hand, quantum finite automata (QFA) emerged as a very elegant and simple model for resolving some quantum computational problems. In this paper, we propose the notion of reactive quantum system (RQS), a variant of QLTS capturing reactive system behavior, and develop a coalgebraic semantics for QLTS, RQS and QFA by an endofunctor on the category of convex sets, which has a final coalgebra. Such a coalgebraic semantics provides a unifying abstract interpretation for QLTS, RQS and QFA. The notions of bisimulation and simulation can be employed to compare the behavior of different types of quantum systems and judge whether a coalgebra can be behaviorally simulated by another.

dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts

Recent advances have shown how decision trees are apt data structures for concisely representing strategies (or controllers) satisfying various objectives. Moreover, they also make the strategy more explainable. The recent tool had provided pipelines with tools supporting strategy synthesis for hybrid systems, such as and . We present , a new version with several fundamentally novel features. Most importantly, the user can now provide domain knowledge to be exploited in the decision tree learning process and can also interactively steer the process based on the dynamically provided information. To this end, we also provide a graphical user interface. It allows for inspection and re-computation of parts of the result, suggesting as well as receiving advice on predicates, and visual simulation of the decision-making process. Besides, we interface model checkers of probabilistic systems, namely and and provide dedicated support for categorical enumeration-type state variables. Consequently, the controllers are more explainable and smaller.