SearcharxivSearch

arXiv subjects

Wan Fokkink

Publications and source records attributed to Wan Fokkink.

At least 19 recordsLinked to original sources

Multimodal Nonblocking Supervisory Control Synthesis

Supervisory control synthesis leverages the nonblocking property to show liveness of the supervised system. This property is particularly weak when system models include fault behavior, reconfiguration, or multiple control goals. To capture a more suitable nonblocking property for such system models, this paper introduces modal and multimodal nonblocking. These novel nonblocking variants impose a restriction on the states visited on the path towards a marked state. Synthesis algorithms are presented to construct modal and multimodal nonblocking supervisors. The novel nonblocking variants are illustrated with three intuitive examples, inspired by real synthesis problems encountered while applying supervisory control synthesis to safety-critical water infrastructures. A comparison is made between the novel nonblocking variants and established nonblocking variants to show that they are distinct. Additionally, where possible, conditions are formulated under which one variant implies the other.

eess.SY

A Fault-Tolerant Version of Safra's Termination Detection Algorithm

Safra's distributed termination detection algorithm employs a logical token ring structure within a distributed network; only passive nodes forward the token, and a counter in the token keeps track of the number of sent minus the number of received messages. We adapt this classic algorithm to make it fault-tolerant. The counter is split into counters per node, to discard counts from crashed nodes. If a node crashes, the token ring is restored locally and a backup token is sent. Nodes inform each other of detected crashes via the token. Our algorithm imposes no additional message overhead, tolerates any number of crashes as well as simultaneous crashes, and copes with crashes in a decentralized fashion. Correctness proofs are provided of both the original Safra's algorithm and its fault-tolerant variant, as well as a model checking analysis.

cs.DC

Overview and Performance Evaluation of Supervisory Controller Synthesis with Eclipse ESCET v4.0

Supervisory controllers control cyber-physical systems to ensure their correct and safe operation. Synthesis-based engineering (SBE) is an approach to largely automate their design and implementation. SBE combines model-based engineering with computer-aided design, allowing engineers to focus on 'what' the system should do (the requirements) rather than 'how' it should do it (design and implementation). In the Eclipse Supervisory Control Engineering Toolkit (ESCET) open-source project, a community of users, researchers, and tool vendors jointly develop a toolkit to support the entire SBE process, particularly through the CIF modeling language and tools. In this paper, we first provide a description of CIF's symbolic supervisory controller synthesis algorithm, and thereby include aspects that are often omitted in the literature, but are of great practical relevance, such as the prevention of runtime errors, handling different types of requirements, and supporting input variables (to connect to external inputs). Secondly, we introduce and describe CIF's benchmark models, a collection of 23 freely available industrial and academic models of various sizes and complexities. Thirdly, we describe recent improvements between ESCET versions v0.8 (December 2022) and v4.0 (June 2024) that affect synthesis performance, evaluate them on our benchmark models, and show the current practical synthesis performance of CIF. Fourthly, we briefly look at multi-level synthesis, a non-monolithic synthesis approach, evaluate its gains, and show that while it can help to further improve synthesis performance, further performance improvements are still needed to synthesize complex models.

eess.SY

Formal Methods for Mobile Ad Hoc Networks: A Survey

In a mobile ad hoc network (MANET), communication is wireless and nodes can move independently. Properly analyzing the functional correctness, performance, and security of MANET protocols is a challenging task. A wide range of formal specification and analysis techniques have been employed in the analysis of MANET protocols. This survey presents an overview of rigorous formal analysis techniques and their applications, with a focus on MANET routing protocols. Next to functional correctness, also real-time properties and security are considered. Moreover, an overview is given of formal frameworks that target MANETs specifically, as well as mobility models that underlie performance analyses of MANET protocols. The aim is to give a comprehensive and coherent overview of this rather scattered field, in which a variety of rigorous formal methods have been applied to analyze different aspects of a wide range of MANET protocols.

cs.NI

Are Two Binary Operators Necessary to Obtain a Finite Axiomatisation of Parallel Composition?

Bergstra and Klop have shown that bisimilarity has a finite equational axiomatisation over ACP/CCS extended with the binary left and communication merge operators. Moller proved that auxiliary operators are necessary to obtain a finite axiomatisation of bisimilarity over CCS, and Aceto et al. showed that this remains true when Hennessy's merge is added to that language. These results raise the question of whether there is one auxiliary binary operator whose addition to CCS leads to a finite axiomatisation of bisimilarity. We contribute to answering this question in the simplified setting of the recursion-, relabelling-, and restriction-free fragment of CCS. We formulate three natural assumptions pertaining to the operational semantics of auxiliary operators and their relationship to parallel composition, and prove that an auxiliary binary operator facilitating a finite axiomatisation of bisimilarity in the simplified setting cannot satisfy all three assumptions.

cs.LO

Model Properties for Efficient Synthesis of Nonblocking Modular Supervisors

Supervisory control theory provides means to synthesize supervisors for systems with discrete-event behavior from models of the uncontrolled plant and of the control requirements. The applicability of supervisory control theory often fails due to a lack of scalability of the algorithms. The paper proposes a format for the requirements and a method to ensure that the crucial properties of controllability and nonblockingness directly hold, thus avoiding the most computationally expensive parts of synthesis. The method consists of creating a control problem dependency graph and verifying whether it is acyclic. Vertices of the graph are modular plant components, and edges are derived from the requirements. In case of a cyclic graph, potential blocking issues can be localized, so that the original control problem can be reduced to only synthesizing supervisors for smaller partial control problems. The strength of the method is illustrated on two case studies: a production line and a roadway tunnel.

eess.SY

A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity

Robin Milner (1984) gave a sound proof system for bisimilarity of regular expressions interpreted as processes: Basic Process Algebra with unary Kleene star iteration, deadlock 0, successful termination 1, and a fixed-point rule. He asked whether this system is complete. Despite intensive research over the last 35 years, the problem is still open. This paper gives a partial positive answer to Milner's problem. We prove that the adaptation of Milner's system over the subclass of regular expressions that arises by dropping the constant 1, and by changing to binary Kleene star iteration is complete. The crucial tool we use is a graph structure property that guarantees expressibility of a process graph by a regular expression, and is preserved by going over from a process graph to its bisimulation collapse.

cs.LO

Divide and Congruence III: From Decomposition of Modal Formulas to Preservation of Stability and Divergence

In two earlier papers we derived congruence formats with regard to transition system specifications for weak semantics on the basis of a decomposition method for modal formulas. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. The stability and divergence requirements that are imposed on many of the known weak semantics have so far been outside the realm of this method. Stability refers to the absence of a $τ$-transition. We show, using the decomposition method, how congruence formats can be relaxed for weak semantics that are stability-respecting. This relaxation for instance brings the priority operator within the range of the stability-respecting branching bisimulation format. Divergence, which refers to the presence of an infinite sequence of $τ$-transitions, escapes the inductive decomposition method. We circumvent this problem by proving that a congruence format for a stability-respecting weak semantics is also a congruence format for its divergence-preserving counterpart.

cs.LO

Divide and Congruence II: From Decomposition of Modal Formulas to Preservation of Delay and Weak Bisimilarity

Earlier we presented a method to decompose modal formulas for processes with the internal action $τ$, and congruence formats for branching and $η$-bisimilarity were derived on the basis of this decomposition method. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. In this follow-up paper the decomposition method is enhanced to deal with modal characterisations that contain a modality $\langleε\rangle\langle a\rangleϕ$, to derive congruence formats for delay and weak bisimilarity.

cs.LO

Reliable Restricted Process Theory

Malfunctions of a mobile ad hoc network (MANET) protocol caused by a conceptual mistake in the protocol design, rather than unreliable communication, can often be detected only by considering communication among the nodes in the network to be reliable. In Restricted Broadcast Process Theory, which was developed for the specification and verification of MANET protocols, the communication operator is lossy. Replacing unreliable with reliable communication invalidates existing results for this process theory. We examine the effects of this adaptation on the semantics of the framework with regard to the non-blocking property of communication in MANETs, the notion of behavioral equivalence relation and its axiomatization. We illustrate the applicability of our framework through a simple routing protocol. To prove its correctness, we introduce a novel proof process, based on a precongruence relation.

cs.LO

On the Axiomatizability of Impossible Futures

A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the process algebra BCCS. This transformation moreover preserves omega-completeness. It is applicable to semantics at least as coarse as impossible futures semantics. As an application, ground- and omega-complete axiomatizations are derived for weak failures, completed trace and trace semantics. We then present a finite, sound, ground-complete axiomatization for the concrete impossible futures preorder, which implies a finite, sound, ground-complete axiomatization for the weak impossible futures preorder. In contrast, we prove that no finite, sound axiomatization for BCCS modulo concrete and weak impossible futures equivalence is ground-complete. If the alphabet of actions is infinite, then the aforementioned ground-complete axiomatizations are shown to be omega-complete. If the alphabet is finite, we prove that the inequational theories of BCCS modulo the concrete and weak impossible futures preorder lack such a finite basis.

cs.LO

Maximally Permissive Controlled System Synthesis for Modal Logic

We propose a new method for controlled system synthesis on non-deterministic automata, which includes the synthesis for deadlock-freeness, as well as invariant and reachability expressions. Our technique restricts the behavior of a Kripke-structure with labeled transitions, representing the uncontrolled system, such that it adheres to a given requirement specification in an expressive modal logic. while all non-invalidating behavior is retained. This induces maximal permissiveness in the context of supervisory control. Research presented in this paper allows a system model to be constrained according to a broad set of liveness, safety and fairness specifications of desired behavior, and embraces most concepts from Ramadge-Wonham supervisory control, including controllability and marker-state reachability. Synthesis is defined in this paper as a formal construction, which allowed a careful validation of its correctness using the Coq proof assistant.

cs.FL

Detecting Useless Transitions in Pushdown Automata

Pushdown automata may contain transitions that are never used in any accepting run of the automaton. We present an algorithm for detecting such useless transitions. A finite automaton that captures the possible stack content during runs of the pushdown automaton, is first constructed in a forward procedure to determine which transitions are reachable, and then employed in a backward procedure to determine which of these transitions can lead to a final stat

cs.FL

Distributed MAP in the SpinJa Model Checker

Spin in Java (SpinJa) is an explicit state model checker for the Promela modelling language also used by the SPIN model checker. Designed to be extensible and reusable, the implementation of SpinJa follows a layered approach in which each new layer extends the functionality of the previous one. While SpinJa has preliminary support for shared-memory model checking, it did not yet support distributed-memory model checking. This tool paper presents a distributed implementation of a maximal accepting predecessors (MAP) search algorithm on top of SpinJa.

cs.SE

Asynchronous Bounded Expected Delay Networks

The commonly used asynchronous bounded delay (ABD) network models assume a fixed bound on message delay. We propose a probabilistic network model, called asynchronous bounded expected delay (ABE) model. Instead of a strict bound, the ABE model requires only a bound on the expected message delay. While the conditions of ABD networks restrict the set of possible executions, in ABE networks all asynchronous executions are possible, but executions with extremely long delays are less probable. In contrast to ABD networks, ABE networks cannot be synchronised efficiently. At the example of an election algorithm, we show that the minimal assumptions of ABE networks are sufficient for the development of efficient algorithms. For anonymous, unidirectional ABE rings of known size N we devise a probabilistic leader election algorithm having average message and time complexity O(N).

cs.DC

A Modeling Framework for Gossip-based Information Spread

We present an analytical framework for gossip protocols based on the pairwise information exchange between interacting nodes. This framework allows for studying the impact of protocol parameters on the performance of the protocol. Previously, gossip-based information dissemination protocols have been analyzed under the assumption of perfect, lossless communication channels. We extend our framework for the analysis of networks with lossy channels. We show how the presence of message loss, coupled with specific topology configurations,impacts the expected behavior of the protocol. We validate the obtained models against simulations for two protocols.

cs.DC

Congruence from the Operator's Point of View: Compositionality Requirements on Process Semantics

One of the basic sanity properties of a behavioural semantics is that it constitutes a congruence with respect to standard process operators. This issue has been traditionally addressed by the development of rule formats for transition system specifications that define process algebras. In this paper we suggest a novel, orthogonal approach. Namely, we focus on a number of process operators, and for each of them attempt to find the widest possible class of congruences. To this end, we impose restrictions on sublanguages of Hennessy-Milner logic, so that a semantics whose modal characterization satisfies a given criterion is guaranteed to be a congruence with respect to the operator in question. We investigate action prefix, alternative composition, two restriction operators, and parallel composition.

cs.LO

Modal Logic and the Approximation Induction Principle

We prove a compactness theorem in the context of Hennessy-Milner logic. It is used to derive a sufficient condition on modal characterizations for the Approximation Induction Principle to be sound modulo the corresponding process equivalence. We show that this condition is necessary when the equivalence in question is compositional with respect to the projection operators.

cs.LO