Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities

We showed in a recent paper that, when verifying a modal $$\mu $$-calculus formula, the actions of the system under verification can be partitioned into sets of so-called weak and strong actions, depending on the combination of weak and strong modalities occurring in the formula. In a compositional verification setting, where the system consists of processes executing in parallel, this partition allows us to decide whether each individual process can be minimized for either divergence-preserving branching (if the process contains only weak actions) or strong (otherwise) bisimilarity, while preserving the truth value of the formula. In this paper, we refine this idea by devising a family of bisimilarity relations, named sharp bisimilarities, parameterized by the set of strong actions. We show that these relations have all the nice properties necessary to be used for compositional verification, in particular congruence and adequacy with the logic. We also illustrate their practical utility on several examples and case-studies, and report about our success in the RERS 2019 model checking challenge.

THE 3D SPIN GEOMETRY OF THE QUANTUM TWO-SPHERE

We study a three-dimensional differential calculus [Formula: see text] on the standard Podleś quantum two-sphere [Formula: see text], coming from the Woronowicz 4D+ differential calculus on the quantum group SU q(2). We use a frame bundle approach to give an explicit description of [Formula: see text] and its associated spin geometry in terms of a natural spectral triple over [Formula: see text]. We equip this spectral triple with a real structure for which the commutant property and the first order condition are satisfied up to infinitesimals of arbitrary order.

Fractional calculus of the $ bar H $-function

The subject of this paper is to derive a fractional calculus formula for $ bar H $-function due to Inayat-Hussain whose based upon generalized fractional integration and differentiation operators of arbitrary complex order involving Appell function $F_3$ due to Saigo & Meada. The results are obtained in a compact form containing the Reimann-Liouville, Eredlyi-Kober and Saigo operators of fractional calculus.

CONSTRUCTIVE CLASSICAL LOGIC AS CPS-CALCULUS

We establish the Curry-Howard isomorphism between constructive classical logic and [Formula: see text]-calculus. [Formula: see text]-calculus exactly means the target language of Continuation Passing Style (CPS) transforms. Constructive classical logic we refer to are LKT and LKQ introduced by Danos et al.(1993).