Performance analysis of probabilistic timed automata using digital clocks

Probabilistic timed automata, a variant of timed automata extended with discrete probability distributions, is a modelling formalism suitable for describing formally both nondeterministic and probabilistic aspects of real-time systems, and is amenable to model checking against probabilistic timed temporal logic properties. However, the previously developed verification algorithms either suffer from high complexity, give only approximate results, or are restricted to a limited class of properties. In the case of classical (non-probabilistic) timed automata it has been shown that for a large class of real-time verification problems correctness can be established using an integral model of time (digital clocks) as opposed to a dense model of time. Based on these results we address the question of under what conditions digital clocks are sufficient for the performance analysis of probabilistic timed automata and show that this reduction is possible for an important class of systems and properties including probabilistic reachability and expected reachability. We demonstrate the utility of this approach by applying the method to the performance analysis of three probabilistic real-time protocols: the dynamic configuration protocol for IPv4 link-local addresses, the IEEE 802.11 wireless local area network protocol and the IEEE 1394 FireWire root contention protocol.

Efficient verification of timed automata with BDD-like data structures

We investigate the effect on efficiency of various design issues for BDD-like data structures of TA state space representation and manipulation. We find that the efficiency is highly sensitive to decision atom design and canonical form definition. We explore the two issues in detail and propose to use CRD (Clock-Restriction Diagram) for TA state space representation and present algorithms for manipulating CRD in the verification of TAs. We compare three canonical forms for zones, develop a procedure for quick zone-containment detection, and present algorithms for verification with backward reachability analysis. Three possible evaluation orderings are also considered and discussed. We implement our idea in our tool Red 4.2 and carry out experiments to compare with other tools and various strategies of Red in both forward and backward analysis. Finally, we discuss the possibility of future improvement.     

基于元胞自动机的增强现实标记识别算法

增强现实系统中标记识别一直是增强现实系统的瓶颈,占用了系统处理的大部分时间,即使采用规则几何形式的标记,对于实时要求很高的增强现实系统而言,其识别算法的效果和实时性也是不理想的,因此提出了一种利用应用元胞自动机模型,利用给定的演化规则,改进在增强现实系统中标记识别的算法,并在ARTOOLKIT系统中做了具体实现.实验结果表明,改进的算法的实时性和识别效果均有了很大的提高.     

A development methodology for embedded systems based on RT-DEVS

This work is concerned with modelling, analysis and implementation of embedded control systems using RT-DEVS, i.e. a specialization of classic discrete event system specification (DEVS) for real-time. RT-DEVS favours model continuity, i.e. the possibility of using the same model for property analysis (by simulation or model checking) and for real time execution. Special case tools are reported in the literature for RT-DEVS model analysis and design. In this work, temporal analysis of a model exploits a translation in Uppaal timed automata for exhaustive verification. For large models a simulator was realized in Java which directly stems from RT-DEVS operational semantics. The same concerns are at the basis of a real-time executive. The paper describes the proposed RT-DEVS development methodology and clarifies its implementation status. The approach is demonstrated by applying it to an embedded system example which is analyzed through model checking and implemented in Java. Finally, research directions which deserve further work are indicated.     

Performance of pipelined asynchronous systems

A testing-based faster-than relation has previously been developed that compares the worst-case efficiency of asynchronous systems. This approach reveals that pipelining does not improve efficiency in general; that it does so in practice depends on assumptions about the user behaviour. Accordingly, the approach was adapted to a setting where user behaviour is known to belong to a specific, but often occurring class of request–response behaviours; some quantitative results on the efficiency of the respective so-called response processes were given. In particular, it was shown that in the adapted setting a very simple case of a pipelined process with two stages is faster than a comparable atomic processing of the two stages.In this paper, we determine the performance of general pipelines, which is not so easy in an asynchronous setting. Pipelines are built with a chaining operator; we also study whether the adapted faster-than relation is compatible with chaining and two other parallel composition operators, and give results on the performance of the respective compositions. These studies also demonstrate how rich the request–respond setting is.     

非线性一次一密(t,n)门限秘密共享方案

针对本身不安全的线性算法构造的门限秘密共享方案存在安全漏洞的问题,以及可信方的参与容易导致单点故障和不可靠情形,结合非线性算法和密码学理论,提出一种无可信方的非线性门限秘密共享方案。方案基于混沌算法和有限状态自动机两种非线性结构,子密钥的产生具有随机性和动态性,参与者可控制每一轮的子密钥来实现一次一密或N次一密安全级别。秘密恢复由拉格朗日插值公式来实现。安全多方计算使各参与者相互牵制,不需可信方参与,满足弹性均衡,可防欺骗与合谋攻击。     

Delay-robustness in distributed control of timed discrete-event systems based on supervisor localisation

Recently, we studied communication delay in distributed control of untimed discrete-event systems based on supervisor localisation. We proposed a property called delay-robustness: the overall system behaviour controlled by distributed controllers with communication delay is logically equivalent to its delay-free counterpart. In this paper, we extend our previous work to timed discrete-event systems, in which communication delays are counted by a special clock event tick. First, we propose a timed channel model and define timed delay-robustness; for the latter, a verification procedure is presented. Next, if the delay-robust property does not hold, we introduce bounded delay-robustness, and present an algorithm to compute the maximal delay bound (measured by number of ticks) for transmitting a channelled event. Finally, we demonstrate delay-robustness on the example of an under-load tap-changing transformer.     

The impact of artificial intelligence on leisure

Two views of AI in leisure and the work-place and two views of society are discussed. There is a conceptualisation of AI systems enhancing people in their work and leisure and another of AI automata which tends to degrade and replace human activity. Researchers tend to resolve into Optimists who work within a micro-sociological view and see AI systems as inevitable and beneficent. Others are Pessimists who adopt a macro-sociological view and see AI in its automata role and deliterious social consequences. These polarised perspectives must be integrated as only enhancing AI is socially acceptable.