Blockchain is an open distributed ledger technology that enables ledger-maintainers on a network to collaboratively synchronize and update their own distributed copies of a single global ledger, with the goal of keeping the ledger copies consistent. This paper presents a theoretical control-model formulation of the founding Satoshi Nakamoto blockchain, aimed at enhancing our operational understanding and development of blockchain systems. The control model is generic of every honest ledger-maintainer's local operations on a blockchain network. The presented research is a logical systematization of operational knowledge that is understandable and explainable for blockchain system engineering and research. Using a software tool supporting a supervisory control theory applied in the formulation, the control model is synthesized and logically validated.

In control of discrete-event systems, translating natural language control requirements into formal specifications in computable graphical form can be error prone, and system designers are often confronted with the longstanding problem of uncertainty in specification formalization, namely: How do we know that such a formalized specification is the one intended? This necessitates specification validation, i.e., manual inspection of the specification's graphical structure to clarify if it formalizes the intended requirement. The uncertainty is compounded in the specification formalization for timed discrete-event systems (TDESs) as timed transition graphs (TTGs), where real-time behavior also needs to be correctly specified. In the fundamental control framework of TDESs, a TTG prescribes a timed regulation of logical behavior restricting a TDES to some timed event-transition sequences. To help validate specification TTGs, we develop a new specification concept of TTG transparency. Our concept formulation embodies the essence of “summarizing” a specification TTG's transition sequences for a TDES, to highlight intermittent transitions essential or relevant for comprehending the specification's nontrivial timed restrictions. The transparency concept governs the reconstruction of a specification TTG into a transparent one. We investigate the problem of maximizing the transparency of specification TTGs for TDESs and show that it is NP-hard. We then develop a polynomial time algorithm for computing a highly transparent TTG. Through two examples, we show that the transparent TTG computed may support specification validation.

A new operational design for hierarchical control of discrete-event systems is proposed. The design brings the structure of command and control from concept to realization for online control operation. For a command reference input, a new concept for output control feasibility of a discrete-event system modeled by a Moore automaton is characterized; and a system decomposition of a suitably structured Moore automaton into a controllable subsystem and an uncontrollable subsystem is formulated. Based on these results, the new command and control design for controller operation is realized, examined, and discussed.

In supervisory control of timed discrete-event systems (TDESs), a conceptually well founded finitary control synthesis framework is developed, and it requires specifications to be prescribed as finite (-trace) automata in the form of timed transition graphs (TTGs). However, prescribing real-time specifications as TTGs is a nontrivial task that must be resolved before the formal framework could expect to become widely used. In addressing this specification problem, metric temporal logic (MTL) is proposed in this paper as a control specification language for use with the TTG-based control synthesis framework. MTL is a designer-friendly formalism due to its human or natural language expressiveness and readability, and is well suited for specifying real-time control specifications. In automating TTG prescription, this paper proposes an MTL interface to the control synthesis framework. The interface is proved to be a correct and complete translation algorithm that converts finitary control specifications written in state-based MTL formulas for a given TDES model into deterministic finite TTGs. Integrated, the MTL interface and the control synthesis framework combine the human expressiveness and readability of MTL with the algorithmic computability of TTGs, and together provide a new and convenient MTL specification-based design tool for automated prescription of TTGs and real-time control synthesis. Illustrative examples demonstrate the utility of the MTL interface.

In datacenter network (DCN) research, one key challenge is to reproduce the relative performances of different scalable DCN architectures in an unbiased and transparent way. Adequately addressing this challenge will support the validation of performance studies, and this is fundamental to building a strong research foundation and making wise datacenter investment decisions. In addressing this challenge, this paper presents the NTU-DSI-DCN initiative with a DCN simulation module based on an open-source platform called ns-3, on which the performance models of DCN topologies can be developed and made open source to support independent reproducibility of their performances. Advantages of the framework include the following: (1) it is low cost, (2) it provides transparent performance benchmarks of known DCN architectures and (3) it enables unbiased comparative performance simulations of DCN architectures, without the tedium of developing existing DCN models from scratch. In realizing this NTU-DSI-DCN initiative, the open-source performance models of the Fat tree and the BCube architectures have been implemented on the ns-3 platform. A comparative performance study between Fat tree and BCube is reported, along with a performance reproducibility study of Fat tree. The documentation and source codes for our simulation setups are publicly available at http://code.google.com/p/ntu-dsidcn/. In continually adding new DCN architectural models or their variants in future work, the NTU-DSI-DCN is a promising initiative that can evolve into a well-documented open-source simulation platform supporting quality research in DCNs.

This paper contributes to the multiagent constraint framework for synthesizing correct local plans and coordination strategies for every participating agent, and meeting their local goals without conflict or blocking. Existing work has focused mainly on developing conflict resolution algorithms for various different types of constraint systems. This paper addresses a new but related problem called multiagent conflict resolution planning for multiple coordination plans. To resolve all potential conflicts between multiagent plans, the problem is to be able to efficiently plan and intelligently select an optimal process plan showing the sequential or partial orders of applying conflict resolution algorithms. A generic approach to the problem is developed that is applicable to various types of constraint systems. Two new innovations are proposed: (1) A comprehensible network model that shows the relationships between agents and their constraints, and (2) a compact AND/OR graph representation of conflict resolution (process) plans. An AND/OR graph plan generation algorithm is proposed and evaluated. The selection of an optimal conflict resolution plan over the AND/OR graph representation is discussed. A case study is presented.

In control of discrete-event systems (DESs), specifying control requirements in automata is not a trivial task. For many DES applications, designers are often confronted with the long-standing problem of uncertainty in specification, namely, how do we know that a specification automaton does indeed model the intended control requirement? Toward a formal framework that helps mitigate this uncertainty for designer comprehensibility, in this paper, we introduce and develop a new specification concept of automaton transparency and investigate the problem of maximizing the transparency of specification automata for DESs. In a transparent specification automaton, events that are irrelevant to the specification but can occur in the system are “hidden” in self-loops. Different automata of the same specification on a DES can be associated with different sets of such irrelevant events, and any such automaton is said to be the most transparent if it has an irrelevant event set of maximal cardinality. The transparency maximization problem is theoretically formulated, and a provably correct solution algorithm is obtained. Given a specification automaton for a DES, the transparent specification automaton produced by the algorithm is a more comprehensible structure, essentially showing the precedence ordering among events from a minimal cardinality set that is relevant in modeling some requirement for the DES, and should aid designers in clarifying if the requirement prescribed is the one intended.

This paper presents new results on the formal design of distributed coordinating agents in a discrete-event framework. In this framework, agents are modeled to be individually equipped with a coordination module, through which they interact and communicate. In terms of existing control-theoretic concepts, we first define the concept of a coordinable language and show that it is the necessary and sufficient existence condition of coordination modules for distributed agents to achieve conformance to a prespecified interagent constraint language. Following, we present a synthesis algorithm to compute near-optimal coordination modules. An example is provided to illustrate the design synthesis using the proposed algorithm. Finally, a discussion with related work distinguishes our coordination design problem from related problems in the literature.

This paper addresses a novel coordination problem for distributed agents in a discrete-event setting. We first introduce and study a predicate coordination problem as the problem of two distributed agents interacting and communicating between themsel

The problem of maximizing the transparency of specification automata for discrete event systems (DES's) is investigated. In a transparent specification automaton, events that are irrelevant to the specification but can occur in the system are `hidden' in self-loops. Different automata of the same specification on a DES can be associated with different sets of such irrelevant events; and any such automaton is said to be the most transparent if it has an irrelevant event set of maximal cardinality. The transparency maximization problem is theoretically formulated and a provably correct solution algorithm is obtained. The most transparent specification automaton essentially shows the precedence ordering among events from a minimal cardinality set that is relevant to the intended requirement, and should help towards resolving the long-standing problem in specification, namely: how do we know that a specification in automata does indeed capture the intended control requirement?

This paper presents a novel multiagent approach to automating taxi dispatch that services current bookings in a distributed fashion. The existing system in use by a taxi operator in Singapore and elsewhere, attempts to increase customer satisfaction locally, by sequentially dispatching nearby taxis to service customers. The proposed dispatch system attempts to increase customer satisfaction more globally, by concurrently dispatching multiple taxis to the same number of customers in the same geographical region, andvis-à-vishuman driver satisfaction. To realize the system, a multiagent architecture is proposed, populated with software collaborative agents that can actively negotiate on behalf of taxi drivers in groups of size N for available customer bookings. Theoretically, an analysis of the boundary and optimal multiagent taxi-dispatch situations is presented along with a discussion of their implications. Experimentally, the operational efficiency of the existing and proposed dispatch systems was evaluated through computer simulations. The empirical results, obtained for a 1000-strong taxi fleet over a discrete range of N , show that the proposed system can dispatch taxis with reduction in customer waiting and empty taxi cruising times of up to 33.1% and 26.3%, respectively; and up to 41.8% and 41.2% reduction when a simple negotiation speedup heuristic was applied.

An empirical and comparative evaluation of multiagent taxi dispatch with extended (E) runtime taxi availability is presented. A taxi in operation is said to be E-runtime available if it has a passenger alighting in ?x > 0 minutes' time or is empty, but has no new committed taxi request to service next. In a multiagent architecture, we consider a new operation policy wherein agents of E-runtime available taxis are allowed to negotiate in individual groups of size N for new taxi requests. The main objective is to present an evaluation of the multiagent system performance gains provided by different times-to-arrival of ?x, under a discrete range of demand rates for several iV-group sizes, as compared with the base case when ?x = 0. It is shown that the proposed policy can effectively reduce customer waiting time and empty taxi cruising time by up to about 60% and 96%, respectively, when the service demand is high for a 1000-strong taxi fleet. It is observed that the value selection for the policy parameter ?x is an important aspect for improving the general performance of multiagent taxi dispatch.

Using dynamic programming (DP), this paper presents a multi-level supervisory control implementation in the standard hierarchical discrete-event control framework. For a class of hierarchically consistent discrete-event systems, the DP algorithm developed implements a multi-level nonblocking controller with reduced off-line complexity of control synthesis and increased on-line transparency of control operations. An example illustrates the on-line control operations of the algorithm.

This paper addresses the collaborative linear- assignment problem (CLAP) for a class of allocation applications. CLAP entails using agents to seek a concurrent allocation of one different object for every agent, to optimize a linear sum efficiency function as their (soft) social goal. Anchoring in the standard framework of automated negotiation allows an original belief-desire-intention (BDI) negotiation model for CLAP to be conceptually separated into a BDI assignment protocol and an adopted strategy. Facilitated by this conceptual separation, the contributions of this paper are as follows: 1) providing a rigorous analysis of the protocol and demonstrating its salient properties and 2) formulating new strategies using a novel idea of cooperative concession. Four different strategies for a negotiation agent and the arbitration agent provide 16 arbitration-negotiation combinations running with the protocol, and these are empirically assessed for their performance profiles in negotiation speed and solution quality. Important findings, including the stability of the protocol in producing better than good enough global allocations and the strategic influence of cooperative concessions on performance, are examined. The significance and practicality of this paper in relation to existing work are also discussed.

This paper presents and analyzes a correct and complete translation algorithm that converts a class of propositional linear-time temporal-logic (PTL) formulae to deterministic finite (-trace) automata. The translation algorithm is proposed as a specification interface for finitary control design of discrete-event systems (DESs). While there has been a lot of computer science research that connects PTL formulae to omega-automata, there is relatively little prior work that translates state-based PTL formulae in the context of a finite-state DES model, to event-based finite automata-the formalism on which well-established control synthesis methods exist. The proposed translation allows control requirements to be more easily described and understood in temporal logic, widely recognized as a useful specification language for its intuitively appealing operators that provide the natural-language expressiveness and readability needed to express and explain these requirements. Adding such a translation interface could therefore effectively combine specifiability and readability in temporal logic with prescriptiveness and computability in finite automata. The former temporal-logic features support specification while the latter automata features support the prescription of DES dynamics and algorithmic computations. A practical implementation of the interface has been developed, providing an enabling technology for writing readable control specifications in PTL that it translates for discrete-event control synthesis in deterministic finite automata. Two application examples illustrate the use of the proposed temporal-logic interface. Practical implications of the complexity of the translation algorithm are discussed.

A new distributed agent algorithm for resource co-allocation to different tasks is proposed. The algorithm extends a belief-desire-intention (BDI) assignment algorithm with resource capability reasoning. It enables resource agents to form coalitions via iterative BDI reasoning and negotiation given the limited capabilities of the resources vis-a-vis task requirements, without directly limiting the coalition size. In the worst case analysis, the number of negotiation rounds required by the algorithm is shown to be of a polynomial order in the number of agents. Empirical evidence from simulations shows that the algorithm yields favorable results in terms of the number of effective coalitions formed for different tasks. Fundamental differences between the proposed algorithm and related work are also discussed.

The collaborative linear assignment problem (CLAP) is a recent framework being developed to provide an intellectual basis for investigating uncluttered agent-based solutions for a fundamental class of combinatorial assignment (or allocation) applications. One key motivation of the research on CLAP is the hope that it can shed new light on adopting agent approaches for solving traditional combinatorial problems in general. To accommodate the various levels of control on agent sociability, typically different application-specific solutions to CLAP are required. In this paper, we take an architectural perspective, classifying solutions according to three typical control structures, namely, centralized, distributed, and decentralized. Existing work focuses mainly on centralized and distributed systems. In this paper, based on the Multi-Agent Assignment Algorithm ({\rm MA}^{3}) used for distributed systems, we propose a new mechanism for a totally decentralized architecture. This proposed mechanism incorporates a novel idea called collaborative Local Mediation (LM), therefore, we term this mechanism {\rm MA}^{3}{\hbox{-}}{\rm{LM}}. We prove that the decentralized {\rm MA}^{3}{\hbox{-}}{\rm{LM}} does not increase the worst-case reasoning complexity when compared to its partially decentralized counterpart. An example illustrates the new mechanism, with emphasis on how it performs collaborative local mediation.

This paper presents a correct and complete algorithm that translates propositional linear time temporal logic (PTL) formulae to event-based automata for finitary control synthesis. It proposes the translation algorithm as a specification interface to well-established automata-theoretic control synthesis methods for discrete-event systems (DES’s). This allows control requirements to be more easily described and understood in an expressive and readable language that temporal logic is widely recognized as. Adding such a translation interface effectively combines specifiability and readability in temporal logic with prescriptiveness and computability in automata. The former temporal logic features support specification while the latter automata features support the prescription of DES dynamics and algorithmic computations. A practical implementation of the interface has been developed, providing an enabling technology for writing more readable control specifications in PTL that it translates for finitary control synthesis in automata. A simple example illustrates the use of the proposed temporal logic interface. Practical implications of the complexity of the translation algorithm are discussed.

This paper proposes and examines a new approach using fuzzy logic to vehicle fleet deployment. Fleet deployment is viewed as a fuzzy linear assignment problem. It assigns each travel request to an available service vehicle through solving a linear assignment matrix of defuzzied cost entries. Each cost entry indicates the cost value of a travel request that "fuzzily aggregates" multiple criteria in simple rules incorporating human dispatching expertise. The approach is examined via extensive simulations anchored in a representative scenario of taxi deployment, and compared to the conventional case of using only distances (each from the taxi position to the source point and finally destination point of a travel request) as cost entries. Discussion in the context of related work examines the performance and practicality of the proposed approach.

In this paper, we propose a supervisory control approach, based on controlled automata concepts, for the planning for online service-operations control of a new class of passenger land-transport systems ( PLanTSs). A PLanTS belongs to a class of dynamic demand-responsive transportation systems. Rapid advances in information and communication technologies are providing a new infrastructural and communications basis upon which higher levels of automation, flexibility, and integration in the development of such transportation systems can be achieved, but to achieve these necessitates the use of more formal approaches for system planning and design. The supervisory control theory of Ramadge and Wonham offers one such methodology, which presents the design for service-operations control as a formal synthesis of a modular supervisory controller. Importantly, the design solution is guaranteed to satisfy the given behavioral specifications in some optimal fashion, without blocking the completion of certain defined "mandatory" tasks. The supervisory design methodology is presented and illustrated in detail via what, in our opinion, is a simplified but realistic PLanTS model. A structural property of the PLanTS model is used to analytically establish the nonblocking property of the modular supervisory controller designed. All automaton models for the PLanTS and the behavioral specifications considered are provided, together with the automata design of the corresponding modular supervisor.

This paper presents a temporal logic formulation of discrete event control which forms a new theoretical basis for control analysis and synthesis of a class of discrete event systems (DES). Specifically, the new basic notions of controllability, control invariance and /spl Sigma//sub u/-invariance are characterized for a safety temporal logic formula, and the necessary and sufficient condition for the existence of its supervisor is established. The existing result based on the predicate approach is shown to be generalized under our formulation. A control synthesis procedure is given for a class of DES based on a specialized safety formula, known as the forbidden state specification. Two simple examples illustrate the proposed axiomatic approach.

A unifying temporal logic framework is proposed for modeling, specifying, and analyzing mechanical assembly sequences. Propositional temporal logic of Manna and Pneuli is the assertion language used for representing and analyzing all constraints or conditions that assembly sequences must satisfy. The generalization of the existing representations through the proposed framework is demonstrated. A new concept of reverse-equivalence, relating assembly and disassembly forms of knowledge, is introduced. It is shown that existing and new assembly sequence properties can be formulated and rigorously proved via mechanical theorem proving based on two assembly process-axioms, and the language inference rules and theorems. Comparison of the proposed framework with the existing representation schemes highlights the main strengths of the proposed framework, viz., temporal expressiveness, strong mechanical manipulation capability and precise formalism. The implementation of the framework on an IPC SUN SPARC workstation using Quintus Prolog for automatic generation of assembly sequences is described. A simple example illustrates the use of the proposed framework for representation, evaluation and selection of feasible assembly sequences.>