Cyberworlds: architecture and modeling by an incrementally modular abstraction hierarchy

An incrementally modular abstraction hierarchy, which specifies, models and visualizes the architecture of cyberworlds from general to specific, is presented. The hierarchy, consisting of a homotopy level with fiber bundles, a set theoretical space level, a topological space level, an adjunction space level, a cellular space level, and presentation and view-levels, is described theoretically with examples of online book shopping such as e-commerce, seat assembling as such e-manufacturing, and accounting such as e-economy. Sharing invariants defined at each level contributes to robust architecture and modeling for designing, analyzing, implementing and visualizing cyberworlds, which results in a fault-free reduction of time and cost.     

The lambda-context calculus (extended version)

We present the Lambda Context Calculus. This simple lambda-calculus features variables arranged in a hierarchy of strengths such that substitution of a strong variable does not avoid capture with respect to abstraction by a weaker variable. This allows the calculus to express both capture-avoiding and capturing substitution (instantiation). The reduction rules extend the ‘vanilla’ lambda-calculus in a simple and modular way and preserve the look and feel of a standard lambda-calculus with explicit substitutions.Good properties of the lambda-calculus are preserved. The LamCC is confluent, and a natural injection into the LamCC of the untyped lambda-calculus exists and preserves strong normalisation.We discuss the calculus and its design with full proofs. In the presence of the hierarchy of variables, functional binding splits into a functional abstraction λ (lambda) and a name-binder и (new). We investigate how the components of this calculus interact with each other and with the reduction rules, with examples. In two more extended case studies we demonstrate how global state can be expressed, and how contexts and contextual equivalence can be naturally internalised using function application.     

The Generating Power of Total Deterministic Tree Transducers

Attributed tree transducers are abstract models used to study properties of attribute grammars. One abstraction which occurs when modeling attribute grammars by attributed tree transducers is that arbitrary trees over a ranked alphabet are taken as input, instead of derivation trees of a context-free grammar. In this paper we show that with respect to the generating power this isnotan abstraction; i.e., we show that attributed tree transducers and attribute grammars generate the same class of term (or tree) languages. To prove this, a number of results concerning the generating power of top-down tree transducers are established, which are interesting in their own. We also show that the classes of output languages of attributed tree transducers form a hierarchy with respect to the number of attributes. The latter result is achieved by proving a hierarchy of classes of tree languages generated by context-free hypergraph grammars with respect to their rank.     

基于多项式符号代数方法的高层次数据通路的等价验证

基于BDD或布尔SAT的等价验证方法虽然能够成功验证低层次门级电路,但却难以满足高层次设计验证要求.由此,以多项式符号代数为理论基础,提出了一个高层次数据通路的等价验证算法.深入研究了使用多项式表达式描述复杂数据通路行为的方法,得到了高层次数据通路的多项式集合表示的一般形式.从多项式集合公共零点的角度定义了高层次数据通路的功能等价,给出了一个基于Gr(o)bner基计算的有效代数求解算法.针对不同基准数据通路的实验结果表明了该算法的有效性.     

Non-Standard Semantics for Program Slicing

In this paper we generalize the notion of compositional semantics to cope with transfinite reductions of a transition system. Standard denotational and predicate transformer semantics, even though compositional, provide inadequate models for some known program manipulation techniques. We are interested in the systematic design of extended compositional semantics, observing possible transfinite computations, i.e. computations that may occur after a given number of infinite loops. This generalization is necessary to deal with program manipulation techniques modifying the termination status of programs, such as program slicing. We include the transfinite generalization of semantics in the hierarchy developed in 1997 by P. Cousot, where semantics at different levels of abstraction are related with each other by abstract interpretation. We prove that a specular hierarchy of non-standard semantics modeling transfinite computations of programs can be specifiedin such a way that the standard hierarchy can be derived by abstract interpretation. We prove that non-standard transfinite denotational and predicate transformer semantics can be both systematically derived as solutions of simple abstract domain equations involving the basic operation of reduced power of abstract domains. This allows us to prove the optimality of these semantics, i.e. they are the most abstract semantics in the hierarchy which are compositional and observe respectively the terminating and initial states of transfinite computations, providing an adequate mathematical model for program manipulation.     

Hierarchical Path Search with Partial Materialization of Costs for a Smart Wheelchair

In this paper, the off-line path planner module of a smart wheelchair aided navigation system is described. Environmental information is structured into a hierarchical graph (H-graph) and used either by the user interface or the path planner module. This information structure facilitates efficient path search and easier information access and retrieval. Special path planning issues like planning between floors of a building (vertical path planning) are also viewed. The H-graph proposed is modelled by a tree. The hierarchy of abstractions contained in the tree has several levels of detail. Each abstraction level is a graph whose nodes can represent other graphs in a deeper level of the hierarchy. Path planning is performed using a path skeleton which is built from the deepest abstraction levels of the hierarchy to the most upper levels and completed in the last step of the algorithm. In order not to lose accuracy in the path skeleton generation and speed up the search, a set of optimal subpaths are previously stored in some nodes of the H-graph (path costs are partially materialized). Finally, some experimental results are showed and compared to traditional heuristic search algorithms used in robot path planning.     

Work domain analysis and sensors I: principles and simple example

In this paper we establish a foundation for understanding the instrumentation needs of complex dynamic systems if ecological interface design (EID)-based interfaces are to be robust in the face of instrumentation failures. EID-based interfaces often include configural displays which reveal the higher-order properties of complex systems. However, concerns have been expressed that such displays might be misleading when instrumentation is unreliable or unavailable. Rasmussen's abstraction hierarchy (AH) formalism can be extended to include representations of sensors near the functions or properties about which they provide information, resulting in what we call a “sensor-annotated abstraction hierarchy”. Sensor-annotated AHs help the analyst determine the impact of different instrumentation engineering policies on higher-order system information by showing how the data provided from individual sensors propagates within and across levels of abstraction in the AH. The use of sensor-annotated AHs with a configural display is illustrated with a simple water reservoir example. We argue that if EID is to be effectively employed in the design of interfaces for complex systems, then the information needs of the human operator need to be considered at the earliest stages of system development while instrumentation requirements are being formulated. In this way, Rasmussen's AH promotes a formative approach to instrumentation engineering.     

带Mismatch算子的高阶π演算

主要研究带mismatch的高阶进程演算的公理化问题。首先,建立存在mismatch时高阶进程的开弱高阶互模拟理论,证明了等价关系、同余性等重要性质;其次,沿用线性的方法,构建得到带 mismatch 的有限进程上的公理系统;最后,基于对开弱高阶互模拟的刻画,证明了该公理系统的完备性定理。该工作为带 mismatch 的高阶进程上互模拟判定的有效算法的设计与实现,进而为相关的应用建模工作提供了理论借鉴。     

Control of nondeterministic discrete-event systems for bisimulation equivalence

Most prior work on supervisory control of discrete event systems is for achieving deterministic specifications, expressed as formal languages. In this paper we study supervisory control for achieving nondeterministic specifications. Such specifications are useful when designing a system at a higher level of abstraction so that lower level details of system and its specification are omitted to obtain higher level models that may be nondeterministic. Nondeterministic specifications are also meaningful when the system to be controlled has a nondeterministic model due to the lack of information (caused for example by partial observation or unmodeled dynamics). Language equivalence is not an adequate notion of behavioral equivalence for nondeterministic systems, and instead we use the finest known notion of equivalence, namely the bisimulation equivalence. Choice of bisimulation equivalence is also supported by the fact that bisimulation equivalence specification is equivalent to a specification in the temporal logic of /spl mu/-calculus that subsumes the complete branching-time logic CTL*. Given nondeterministic models of system and its specification, we study the design of a supervisor (possibly nondeterministic) such that the controlled system is bisimilar to the specification. We obtain a small model theorem showing that a supervisor exists if and only if it exists over a certain finite state space, namely the power set of Cartesian product of system and specification state spaces. Also, the notion of state-controllability is introduced as part of a necessary and sufficient condition for the existence of a supervisor. In the special case of deterministic systems, we provide an existence condition that can be verified polynomially in both system and specification states, when the existence condition holds.     

Levels of abstraction in designs of human–computer interaction: The case of e-mail

People process information at different levels of abstraction (e.g., talking about a topic in general terms and then going into the details). They move from one level to another but focus on a particular level at any specific moment. We see this behavior in the most common of tasks, such as solving problems, communicating and designing. This paper explores the implications of levels of abstraction on designing interactive systems. It demonstrates the idea by showing the feasibility and desirability of building a simple e-mail system based on the idea of levels of abstraction and testing its usability.We believe the implications of levels of abstraction on design are profound as regards the design of interactive systems that support dynamic behavior. Having shown the feasibility of some basic design implications, we call for empirical studies to test their usability and explore more advanced design implications.     

Structure-Preserving Hierarchical Decompositions

A hierarchy tree of a graph G is a rooted tree whose leaves are the vertices of G; the internal nodes are usually called clusters. Hierarchy trees are well suited for representing hierarchical decompositions of graphs. In this paper we introduce the notion of P-validity of hierarchy trees with respect to a given graph property P. This notion reflects the similarity between any high-level representation of G obtained from the hierarchy tree and the topological structure of G. Maintaining the properties of a graph at any level of abstraction is especially relevant in graph drawing applications. We present a structural characterization of P-valid hierarchy trees when the clustered graph is a tree and property P is the acyclicity. Besides being interesting in its own right, our structure theorem can be used in the design of a polynomial time algorithm for recognizing P-valid hierarchy trees.     

Representation of heterogeneous material properties in the Core Product Model

The Core Product Model (CPM) was developed at National Institute of Standards as a high level abstraction for representing product related information, to support data exchange, in a distributive and a collaborative environment. In this paper, we extend the CPM to components with continuously varying material properties. Such components are becoming increasing important and popular due to progress in design, analysis and manufacturing techniques. The key enabling concept for modeling continuously varying material properties is that of distance fields associated with a set of material features, where values and rates of material properties are specified. Material fields, representing distribution of material properties within a component, are usually expressed as functions of distances to material features, and are controlled with a variety of differential, integral or algebraic constraints. Our formulation is independent of any particular platform or representation, and applies to most proposed techniques for representing continuously varying material properties. The proposed model is described using Unified Modeling Language and is illustrated through a number of specific examples.     

Abstractions of Hamiltonian control systems

Given a control system and a desired property, an abstracted system is a reduced system that preserves the property of interest while ignoring modeling detail. In previous work, abstractions of linear and nonlinear control systems were considered while preserving reachability properties. In this paper, we consider the abstraction problem for Hamiltonian control systems, where, in addition to the property of interest we also preserve the Hamiltonian structure of the control system. We show how the Hamiltonian structure of control systems can be exploited to simplify the abstraction process. We then focus on local accessibility preserving abstractions, and provide conditions under which local accessibility properties of the abstracted Hamiltonian system are equivalent to the local accessibility properties of the original Hamiltonian control system.     

Local Invariance

A local invariant is a set of states of a transition system with the property that every action possible from each of its states takes the system back into the local invariant, unless it is an ‘exit’ action, each of which is accessible from every state in the set via a sequence of non-‘exit’ actions. This idea supports a form of abstraction construction, abstracting away from behaviour internal to the local invariants themselves, that involving their non-‘exit’ actions. In this way, for example, it is possible to construct from a system one which exhibits precisely the externally visible behaviour. This abstraction is reminiscent of hiding in process algebra, and we compare the notion of abstraction with that of observational equivalence in process calculus. Received August 2000 / Accepted in revised form March 2002 Correspondence and offprint requests to: David H. Pitt, Department of Computing, University of Surrey, Guildford GU2 5HX, UK. E-mail: d.pitt@eim.surrey.ac.ukau     

Making sense of the abstraction hierarchy in the power plant domain

The paper discusses the abstraction hierarchy proposed by Rasmussen [(1986) Information processing and human-machine interaction, North-Holland] for design of human-machine interfaces for supervisory control. The purpose of the abstraction hierarchy is to represent a work domain by multiple levels of means-end and part-whole abstractions. It is argued in the paper that the abstraction hierarchy suffers from both methodological and conceptual problems. A cluster of selected problems are analyzed and illustrated by concrete examples from the power plant domain. It is concluded that the semantics of the means-end levels and their relations are vaguely defined and therefore should be improved by making more precise distinctions. Furthermore, the commitment to a fixed number of levels of means-end abstractions should be abandoned and more attention given to the problem of level identification in the model-building process. It is also pointed out that attempts to clarify the semantics of the abstraction hierarchy will invariably reduce the range of work domains where it can be applied.     

A Small Model Theorem for Bisimilarity Control Under Partial Observation

This paper extends our prior result on decidability of bisimulation equivalence control from the setting of complete observations to that of partial observations. Besides being control compatible, the supervisor must now also be observation compatible. We show that the "small model theorem" remains valid by showing that a control and observation compatible supervisor exists if and only if it exists over a certain finite state space, namely the power set of the Cartesian product of the system and the specification state spaces. Note to Practitioners-Non-determinism in discrete-event systems arises due to abstraction and/or unmodeled dynamics. This paper addresses the issue of control of non-deterministic systems subject to non-deterministic specifications, under a partial observation of events. Non-deterministic plant and specification are useful when designing a system at a higher level of abstraction so that lower level details of the system and its specification are omitted to obtain higher level models that are non-deterministic. The control goal is to ensure that the controlled system has an equivalent behavior as the specification system, where the notion of equivalence used is that of bisimilarity. Bisimilarity requires the existence of an equivalence relation between the states of the two systems so that transitions on common events beginning from a pair of equivalent states end up in a pair of equivalent successor states. Supervisors are also allowed to be nondeterministic, where the nondeterminism in control is implemented by selecting control actions nondeterministically from among a set of precomputed choices. The main contribution of this paper is to show that a supervisor exists if and only if one exists where the size of its state-space upper bounded and so it suffices to search over this state space. We illustrate our results through a manufacturing example     

Non‐blocking decentralized control of discrete event systems based on Petri nets

The non‐blocking property of discrete event systems can formulate many practical and important properties of manufacturing systems, such as deadlock freeness, liveness and reversibility. But it is difficult to guarantee non‐blocking control. This paper presents a hybrid approach to decentralized control of discrete event systems. More generalized constraints are considered in this approach, which gives a graphical way of designing coordinators to keep the non‐blocking property of the closed‐loop system with decentralized supervisors. This approach also guarantees that the closed‐loop system is maximally permissive. Copyright © 2010 John Wiley and Sons Asia Pte Ltd and Chinese Automatic Control Society     

Encoding, Decoding and Data Refinement

Data refinement is the systematic replacement of a data structure with another one in program development. Data refinement between program statements can on an abstract level be described as a commutativity property where the abstraction relationship between the data structures involved is represented by an abstract statement (a decoding). We generalise the traditional notion of data refinement by defining an encoding operator that describes the least (most abstract) data refinement with respect to a given abstraction. We investigate the categorical and algebraic properties of encoding and describe a number of special cases, which include traditional notions of data refinement. The dual operator of encoding is decoding, which we investigate and give an intuitive interpretation to. Finally we show a number of applications of encoding and decoding. Received May 1999 / Accepted in revised form November 2000