Computing crisp simulations for fuzzy labeled transition systems

2021 ◽  
pp. 1-12
Author(s):  
Linh Anh Nguyen
Keyword(s):  
Efficient Algorithm ◽  
Transition System ◽  
Worst Case ◽  
Transition Systems ◽  
Fuzzy Automata ◽  
Labeled Transition System ◽  
The Given ◽  
Naive Approach

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.

scholarly journals Local Model Checking and Traces

1994 ◽  
Vol 1 (17) ◽  
Author(s):  
Allan Cheng
Keyword(s):  
Model Checking ◽  
Polynomial Time ◽  
Transition System ◽  
Satisfiability Problem ◽  
Local Model ◽  
Transition Systems ◽  
Finite Systems ◽  
Soundness And Completeness ◽  
The Given ◽  
Local Model Checking

We present a <em>CTL</em>-like logic which is interpreted over labeled asynchronous transition systems. The interpretation reflects the desire to reason about these only with respect their progress fair behaviours. For finite systems we provide a set of tableau rules and prove soundness and completeness with respect to the given interpretation of our logic. We also provide a model checking algorithm which solves the model checking problem in deterministic polynomial time in the size of the formula and the labelled asynchronous transition system. We then consider different extensions of the logic with modalities expressing concurrent behaviour and investigate how this affects the decidability of the satisfiability problem.

scholarly journals Parallel One-Step Control of Parametrised Boolean Networks

Mathematics ◽  
2021 ◽  
Vol 9 (5) ◽  
pp. 560 ◽  
Author(s):  
Luboš Brim ◽  
Samuel Pastva ◽  
David Šafránek ◽  
Eva Šmijáková
Keyword(s):  
Control Problem ◽  
Boolean Networks ◽  
Actual State ◽  
Worst Case ◽  
Symbolic Data ◽  
One Step ◽  
The One ◽  
Step Control ◽  
Symbolic Algorithm ◽  
Naive Approach

Boolean network (BN) is a simple model widely used to study complex dynamic behaviour of biological systems. Nonetheless, it might be difficult to gather enough data to precisely capture the behavior of a biological system into a set of Boolean functions. These issues can be dealt with to some extent using parametrised Boolean networks (ParBNs), as this model allows leaving some update functions unspecified. In our work, we attack the control problem for ParBNs with asynchronous semantics. While there is an extensive work on controlling BNs without parameters, the problem of control for ParBNs has not been in fact addressed yet. The goal of control is to ensure the stabilisation of a system in a given state using as few interventions as possible. There are many ways to control BN dynamics. Here, we consider the one-step approach in which the system is instantaneously perturbed out of its actual state. A naïve approach to handle control of ParBNs is using parameter scan and solve the control problem for each parameter valuation separately using known techniques for non-parametrised BNs. This approach is however highly inefficient as the parameter space of ParBNs grows doubly exponentially in the worst case. We propose a novel semi-symbolic algorithm for the one-step control problem of ParBNs, that builds on symbolic data structures to avoid scanning individual parameters. We evaluate the performance of our approach on real biological models.

Parametric Kinematic Tolerance Analysis of Planar Pairs With Multiple Contacts

1996 ◽  
Author(s):  
Elisha Sacks ◽  
Leo Joskowicz
Keyword(s):  
Efficient Algorithm ◽  
Tolerance Analysis ◽  
Parametric Model ◽  
Worst Case ◽  
Multiple Contacts ◽  
Work Cycle ◽  
Computer Aided ◽  
Kinematic Models ◽  
Range Of Variation ◽  
Different Parts

Abstract We present an efficient algorithm for worst-case limit kinematic tolerance analysis of planar kinematic pairs with multiple contacts. The algorithm extends computer-aided kinematic tolerance analysis from mechanisms in which parts interact through permanent contacts to mechanisms in which different parts or part features interact at different stages of the work cycle. Given a parametric model of a pair and the range of variation of the parameters, it constructs parametric kinematic models for the contacts, computes the configurations in which each contact occurs, and derives the sensitivity of the kinematic variation to the parameters. The algorithm also derives qualitative variations, such as under-cutting, interference, and jamming. We demonstrate the algorithm on a 26 parameter model of a Geneva mechanism.

scholarly journals Angle Bisector Algorithm and Modified Dynamic Programming Algorithm for Dubins Traveling Salesman Problem

2021 ◽  
Author(s):  
Eswara Venkata Kumar Dhulipala
Keyword(s):  
Euclidean Distance ◽  
Travelling Salesman Problem ◽  
Dynamic Programming Algorithm ◽  
Constant Factor ◽  
Programming Algorithm ◽  
Worst Case ◽  
Angle Bisector ◽  
Set Of Points ◽  
The Given ◽  
Tour Length

A Dubin's Travelling Salesman Problem (DTSP) of finding a minimum length tour through a given set of points is considered. DTSP has a Dubins vehicle, which is capable of moving only forward with constant speed. In this paper, first, a worst case upper bound is obtained on DTSP tour length by assuming DTSP tour sequence same as Euclidean Travelling Salesman Problem (ETSP) tour sequence. It is noted that, in the worst case, \emph{any algorithm that uses of ETSP tour sequence} is a constant factor approximation algorithm for DTSP. Next, two new algorithms are introduced, viz., Angle Bisector Algorithm (ABA) and Modified Dynamic Programming Algorithm (MDPA). In ABA, ETSP tour sequence is used as DTSP tour sequence and orientation angle at each point $i_k$ are calculated by using angle bisector of the relative angle formed between the rays $i_{k}i_{k-1}$ and $i_ki_{k+1}$. In MDPA, tour sequence and orientation angles are computed in an integrated manner. It is shown that the ABA and MDPA are constant factor approximation algorithms and ABA provides an improved upper bound as compared to Alternating Algorithm (AA) \cite{savla2008traveling}. Through numerical simulations, we show that ABA provides an improved tour length compared to AA, Single Vehicle Algorithm (SVA) \cite{rathinam2007resource} and Optimized Heading Algorithm (OHA) \cite{babel2020new,manyam2018tightly} when the Euclidean distance between any two points in the given set of points is at least $4\rho$ where $\rho$ is the minimum turning radius. The time complexity of ABA is comparable with AA and SVA and is better than OHA. Also we show that MDPA provides an improved tour length compared to AA and SVA and is comparable with OHA when there is no constraint on Euclidean distance between the points. In particular, ABA gives a tour length which is at most $4\%$ more than the ETSP tour length when the Euclidean distance between any two points in the given set of points is at least $4\rho$.

scholarly journals State Complexity of Neighbourhoods and Approximate Pattern Matching

2018 ◽  
Vol 29 (02) ◽  
pp. 315-329 ◽  
Author(s):  
Timothy Ng ◽  
David Rappaport ◽  
Kai Salomaa
Keyword(s):  
Lower Bound ◽  
Pattern Matching ◽  
Finite Automaton ◽  
The State ◽  
Worst Case ◽  
State Complexity ◽  
Approximate Pattern Matching ◽  
The Given ◽  
Nondeterministic Finite Automaton ◽  
Distance Formula

The neighbourhood of a language [Formula: see text] with respect to an additive distance consists of all strings that have distance at most the given radius from some string of [Formula: see text]. We show that the worst case deterministic state complexity of a radius [Formula: see text] neighbourhood of a language recognized by an [Formula: see text] state nondeterministic finite automaton [Formula: see text] is [Formula: see text]. In the case where [Formula: see text] is deterministic we get the same lower bound for the state complexity of the neighbourhood if we use an additive quasi-distance. The lower bound constructions use an alphabet of size linear in [Formula: see text]. We show that the worst case state complexity of the set of strings that contain a substring within distance [Formula: see text] from a string recognized by [Formula: see text] is [Formula: see text].

Target-oriented Petri Net Synthesis

2020 ◽  
Author(s):  
Eike Best ◽  
Raymond Devillers ◽  
Evgeny Erofeev ◽  
Harro Wimmel
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
Transition System ◽  
Efficient Synthesis ◽  
Transition Systems ◽  
Np Complete ◽  
Full Class ◽  
Petri Net Synthesis ◽  
Labelled Transition System ◽  
Additional Constraints

When a Petri net is synthesised from a labelled transition system, it is frequently desirable that certain additional constraints are fulfilled. For example, in circuit design, one is often interested in constructing safe Petri nets. Targeting such subclasses of Petri nets is not necessarily computationally more efficient than targeting the whole class. For example, targeting safe nets is known to be NP-complete while targeting the full class of place/transition nets is polynomial, in the size of the transition system. In this paper, several classes of Petri nets are examined, and their suitability for being targeted through efficient synthesis from labelled transition systems is studied and assessed. The focus is on choice-free Petri nets and some of their subclasses. It is described how they can be synthesised efficiently from persistent transition systems, summarising and streamlining in tutorial style some of the authors’ and their groups’ work over the past few years.

Service Discovery and Composition Based on Contracts and Choreographic Descriptions

2012 ◽  
pp. 60-88
Author(s):  
Mario Bravetti ◽  
Gianluigi Zavattaro
Keyword(s):  
Service Discovery ◽  
Operational Semantics ◽  
Asynchronous Communication ◽  
Synchronous Communication ◽  
Transition Systems ◽  
Service Contracts ◽  
Contract Compliance ◽  
Service Oriented ◽  
Labeled Transition System ◽  
Contract Language

The authors discuss the interplay between the notions of contract compliance, contract refinement, and choreography conformance in the context of service oriented computing, by considering both synchronous and asynchronous communication. Service contracts are specified in a language independent way by means of finite labeled transition systems. In this way, the theory is general and foundational as the authors abstract away from the syntax of contracts and simply assume that a contract language has an operational semantics defined in terms of a labeled transition system. The chapter makes a comparative analysis of synchronous and asynchronous communication. Concerning the latter, a realistic scenario is considered in which services are endowed with queues used to store the received messages. In the simpler context of synchronous communication, the authors are able to resort to the theory of fair testing to provide decidability results.

Fuzzy Labeled Transition Refinement Tree

2014 ◽  
Vol 6 (3) ◽  
pp. 1-31 ◽  
Author(s):  
Sofia Kouah ◽  
Djamel-Eddine Saidouni
Keyword(s):  
Dynamic Systems ◽  
Transition System ◽  
System Model ◽  
Design Parameters ◽  
Concurrent Design ◽  
Incremental Development ◽  
Action Refinement ◽  
Formal Framework ◽  
Labeled Transition System ◽  
Multi Agents

This paper aims to provide a formal framework that supports an incremental development of dynamic systems such as multi agents systems (MAS). We propose a fuzzy labeled transition system model (FLTS for short). FLTS allows a concise action refinement representation and deals with incomplete information through its fuzziness representation. Afterward, based on FLTS model, we propose a refinement model called fuzzy labeled transition refinement tree (FLTRT for short). The FLTRT structure serves as a tree of potential concurrent design trajectories of the system. Also, we introduce bisimulation relations for both models in order to identify equivalent design trajectories, which could be assessed with respect to relevant design parameters.

Hierarchical Design Method for Multi-Agent Systems

2015 ◽  
Vol 7 (2) ◽  
pp. 105-134
Author(s):  
Bouneb Messaouda ◽  
Saïdouni Djamel Eddine
Keyword(s):  
Design Methodology ◽  
Design Method ◽  
Transition System ◽  
Hierarchical Design ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Multi Agent ◽  
Labeled Transition System ◽  
System Assessment ◽  
Definition Of

This paper proposes a new hierarchical design method for the specification and the verification of multi agent systems (MAS). For this purpose, the authors propose the model of Refinable Recursive Petri Nets (RRPN) under a maximality semantics. In this model, a notion of undefined transitions is considered. The underlying semantics model is the Abstract Maximality-based Labeled Transition System (AMLTS). Hence, the model supports a definition of a hierarchical design methodology. The example of goods transportation is used for illustrating the approach. For the system assessment, the properties are expressed in CTL logic and verified using the verification environment FOCOVE (Formal Concurrency Verification Environment).

Application of Fuzzy Labeled Transition System to Contract Net Protocol

2015 ◽  
Vol 6 (3) ◽  
pp. 27-46 ◽  
Author(s):  
Sofia Kouah ◽  
Djamel Eddine Saïdouni
Keyword(s):  
Dynamic Systems ◽  
Transition System ◽  
Multi Agent Systems ◽  
Contract Net Protocol ◽  
Agent Systems ◽  
Contract Net ◽  
Multi Agent ◽  
Refinement Process ◽  
Labeled Transition System

For developing large dynamic systems in a rigorous manner, fuzzy labeled transition refinement tree (FLTRT for short) has been defined. This model provides a formal specification framework for designing such systems. In fact, it supports abstraction and enables fuzziness which allows a rigorous formal refinement process. The purpose of this paper is to illustrate the applicability of FLTRT for designing multi agent systems (MAS for short), among others collective and internal agent's behaviors. Therefore, Contract Net Protocol (CNP for short) is chosen as case study.

Sign in / Sign up

Export Citation Format

Share Document