The Complexity of Synthesis of b-Bounded Petri Nets

For a fixed type of Petri nets τ, τ-SYNTHESIS is the task of finding for a given transition system A a Petri net N of type τ(τ-net, for short) whose reachability graph is isomorphic to A if there is one. The decision version of this search problem is called τ-SOLVABILITY. If an input A allows a positive decision, then it is called τ-solvable and a sought net N τ-solves A. As a well known fact, A is τ-solvable if and only if it has the so-called τ-event state separation property (τ-ESSP, for short) and the τ-state separation property (τ-SSP, for short). The question whether A has the τ-ESSP or the τ-SSP defines also decision problems. In this paper, for all b ∈ ℕ, we completely characterize the computational complexity of τ-SOLVABILITY, τ-ESSP and τ-SSP for the types of pure b-bounded Place/Transition-nets, the b-bounded Place/Transitionnets and their corresponding ℤb+1-extensions.

A Novel Embedding Model Based on a Transition System for Building Industry-Collaborative Digital Twin

Recently, the production environment has been rapidly changing, and accordingly, correct mid term and short term decision-making for production is considered more important. Reliable indicators are required for correct decision-making, and the manufacturing cycle time plays an important role in manufacturing. A method using digital twin technology is being studied to implement accurate prediction, and an approach utilizing process discovery was recently proposed. This paper proposes a digital twin discovery framework using process transition technology. The generated digital twin will unearth its characteristics in the event log. The proposed method was applied to actual manufacturing data, and the experimental results demonstrate that the proposed method is effective at discovering digital twins.

Impact Analysis of Transition between Semi-Rigid and Rigid Barriers Using Simulations

Transition is a type of barrier that connects other barriers with different grades and shapes. Even if each barrier satisfies the performance, it may not be satisfied in transition. Therefore, collision safety requires a special design and examination. In this study, we investigated national and foreign standards and situations for the proper configuration of the transition and analyzed the impact behavior of the general transition using impact simulations. We developed a transition system that could ensure the stable performance of various grades by analyzing the behavior and confirmed based on the full-scale crash test (SB2 level).

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.

A Quick Start Method for MEMS Disk Resonant Gyroscope

High-precision disk resonator gyroscope has a high quality factor in order to improve the performance of the gyroscope, as the high quality factor can lead to a long starting time. In this paper, a control system of the driving loop of the disk MEMS resonant gyroscope with the quick start is designed. The control system has functions of quick frequency locking and fast step response. Coarse-precision mode transition system is designed for quick frequency locking. A large-small mode transition system is designed for fast step response. The correctness of the design is verified by circuit test. The test results show that the start-up time is reduced by over 80% compared with the traditional control loop.

Knowledge Dynamics and Behavioural Equivalencesin Multi-Agent Systems

We define a process calculus to describe multi-agent systems with timeouts for communication and mobility able to handle knowledge. The knowledge of an agent is represented as sets of trees whose nodes carry information; it is used to decide the interactions with other agents. The evolution of the system with exchanges of knowledge between agents is presented by the operational semantics, capturing the concurrent executions by a multiset of actions in a labelled transition system. Several results concerning the relationship between the agents and their knowledge are presented. We introduce and study some specific behavioural equivalences in multi-agent systems, including a knowledge equivalence able to distinguish two systems based on the interaction of the agents with their local knowledge.

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.

Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs

Search-based satisfiability procedures try to build a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. Conflict-driven procedures perform non-trivial inferences only when resolving conflicts between formulæ and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability) is a method for conflict-driven reasoning in unions of theories. It combines inference systems for individual theories as theory modules within a solver for the union of the theories. This article augments CDSAT with a more general lemma learning capability and with proof generation. Furthermore, theory modules for several theories of practical interest are shown to fulfill the requirements for completeness and termination of CDSAT. Proof generation is accomplished by a proof-carrying version of the CDSAT transition system that produces proof objects in memory accommodating multiple proof formats. Alternatively, one can apply to CDSAT the LCF approach to proofs from interactive theorem proving, by defining a kernel of reasoning primitives that guarantees the correctness by construction of CDSAT proofs.