Articulations and Products of Transition Systems and their Applications to Petri Net Synthesis

In order to speed up the synthesis of Petri nets from labelled transition systems, a divide and conquer strategy consists in defining decompositions of labelled transition systems, such that each component is synthesisable iff so is the original system. Then corresponding Petri Net composition operators are searched to combine the solutions of the various components into a solution of the original system. The paper presents two such techniques, which may be combined: products and articulations. They may also be used to structure transition systems, and to analyse the performance of synthesis techniques when applied to such structures.

Expressive Logics for Coinductive Predicates

The classical Hennessy-Milner theorem says that two states of an image-finite transition system are bisimilar if and only if they satisfy the same formulas in a certain modal logic. In this paper we study this type of result in a general context, moving from transition systems to coalgebras and from bisimilarity to coinductive predicates. We formulate when a logic fully characterises a coinductive predicate on coalgebras, by providing suitable notions of adequacy and expressivity, and give sufficient conditions on the semantics. The approach is illustrated with logics characterising similarity, divergence and a behavioural metric on automata.

Using Transition Systems to Formalise Ideas from Vedanta

Vedanta is one of the oldest philosophical systems. While there are many detailed commentaries on Vedanta, there are very few mathematical descriptions of the different concepts developed there. This article shows how ideas from theoretical computer science can be used to explain Vedanta. The standard idea of transition systems and modal logic are used to develop a formal description for the different ideas in Vedanta. The generality of the formalism is illustrated via a number of examples including \samsara, \Patanjali's yoga sutras, karma, the three avasthas from the Mandukya Upanishad and the key difference between advaita and dvaita in relation to moksha.

Strain induced localization to delocalization transition on a Lieb photonic ribbon lattice

Ribbon lattices are kind of transition systems in between one and two dimensions, and their study is crucial to understand the origin of different emerging properties. In this work, we study a Lieb ribbon lattice and the localization–delocalization transition occurring due to a reduction of lattice distances (compression) and the corresponding flat band deformation. We observe how above a critical compression ratio the energy spreads out and propagates freely across the lattice, therefore transforming the system from being a kind of insulator into a conductor. We implement an experiment on a photonic platform and show an excellent agreement with the predicted phenomenology. Our findings suggest and prove experimentally the use of compression or mechanical deformation of lattices to switch the transport properties of a given system.

Computing crisp simulations for fuzzy labeled transition systems

The problem of checking whether a state in a finite fuzzy labeled transition system (FLTS) crisply simulates another is one of the fundamental problems of the theory of FLTSs. This problem is of the same nature as computing the largest crisp simulation between two finite FLTSs. A naive approach to the latter problem is to crisp the given FLTSs and then apply one of the currently known best methods to the obtained crisp labeled transition systems. The complexity of the resulting algorithms is of order O (l (m + n) n), where l is the number of fuzzy values occurring in the specification of the input FLTSs, m is the number of transitions and n is the number of states of the input FLTSs. In the worst case, l can be m + n and O (l (m + n) n) is the same as O ((m + n) 2 n). In this article, we design an efficient algorithm with the complexity O ((m + n) n) for computing the largest crisp simulation between two finite FLTSs. This gives a significant improvement. We also adapt our algorithm to computing the largest crisp simulation between two finite fuzzy automata.

Strain-induced Localization-delocalization Transition on a Lieb Ribbon Lattice

Ribbon lattices are kind of transition systems in between one and two dimensions, and their study is crucial to understand the origin of different emerging properties. In this work, we study a Lieb ribbon lattice and the localization-delocalization transition occurring due to a reduction of lattice distances (compression) and the corresponding flat band deformation. We observe how above a critical compression ratio the energy spreads out and propagates freely across the lattice, therefore transforming the system from being a kind of insulator into a conductor. We implement an experiment on a photonic platform and show an excellent agreement with the predicted phenomenology. Our findings suggest and prove experimentally the use of compression or mechanical deformation of lattices to switch the transport properties of a given system.

Modular coinduction up-to for higher-order languages via first-order transition systems

The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on abstract fixed-point theory and compatible functions. We transport this theory onto languages whose bisimilarity and LTS go beyond those of first-order models. The approach consists in exhibiting fully abstract translations of the more sophisticated LTSs and bisimilarities onto the first-order ones. This allows us to reuse directly the large corpus of up-to techniques that are available on first-order LTSs. The only ingredient that has to be manually supplied is the compatibility of basic up-to techniques that are specific to the new languages. We investigate the method on the pi-calculus, the lambda-calculus, and a (call-by-value) lambda-calculus with references.

Vacuity in synthesis

In reactive synthesis, one begins with a temporal specification $$\varphi $$ φ , and automatically synthesizes a system $$M$$ M such that $$M\models \varphi $$ M ⊧ φ . As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity. Our conjecture is that if the synthesized system M satisfies $$\varphi $$ φ non-vacuously, then M is likely to be closer to the user’s intent, because it satisfies $$\varphi $$ φ in a more “meaningful” way. Narrowing the gap between the formal specification and the designer’s intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.