Completeness of a first-order temporal logic with time-gaps

The first-order temporal logics with □ and ○ of time structures isomorphic to ω (discrete linear time) and trees of ω-segments (linear time with branching gaps) and some of its fragments are compared: the first is not recursively axiomatizable. For the second, a cut-free complete sequent calculus is given, and from this, a resolution system is derived by the method of Maslov.     

Parameterized verification of leader/follower systems via first-order temporal logic

Formal Methods in System Design - We introduce a framework for the verification of protocols involving a distinguished machine (referred to as a leader) orchestrating the operation of an arbitrary...     

Intelligent and pervasive computing for cyber-physical systems

The Journal of Supercomputing -     

Understanding mass participatory pervasive computing systems for environmental campaigns

Participate was a 3-year collaboration between industry and academia to explore how mobile, Web and broadcast technologies could combine to deliver environmental campaigns. In a series of pilot projects, schools used mobile sensors to enhance science learning; visitors to an ecological attraction employed mobile phones to access and generate locative media; and the public played a mobile phone game that challenged their environmental behaviours. Key elements of these were carried forward into an integrated trial in which participants were assigned a series of environmental missions as part of an overarching narrative that was delivered across mobile, broadcast and Web platforms. These experiences use a three-layered structure for campaigns that draw on experts, local groups and the general public, who engage through a combination of playful characterisation and social networking.     

Bandwidth scavenging for device coexistence in pervasive computing systems

Opportunistic Spectrum Access in a pervasive computing system can enable a set of secondary user devices to access unused spectrum, or whitespace, found between the transmissions of a set of primary user devices. The design objective for an efficient secondary user access strategy is to be able to “scavenge” spatio-temporally fragmented bandwidth while limiting the amount of disruption caused to the primary user devices. In this paper, we propose an access strategy which is based on measurement and modeling of the whitespace as perceived by the secondary user devices. A secondary user device continually monitors and models its surrounding whitespace, and then accesses the available spectrum so that the effective secondary throughput is maximized while the resulting disruption to the primary user devices is limited to a pre-defined bound. We first develop analytical expressions for the secondary throughput and primary disruption, and then perform ns2 based simulation experiments to validate its effectiveness under various topologies, user traffic profiles, and secondary user populations.     

Cut-free sequent systems for temporal logic

Currently known sequent systems for temporal logics such as linear time temporal logic and computation tree logic either rely on a cut rule, an invariant rule, or an infinitary rule. The first and second violate the subformula property and the third has infinitely many premises. We present finitary cut-free invariant-free weakening-free and contraction-free sequent systems for both logics mentioned. In the case of linear time all rules are invertible. The systems are based on annotating fixpoint formulas with a history, an approach which has also been used in game-theoretic characterisations of these logics.     

Multipurpose prototypes for assessing user interfaces in pervasive computing systems

In pervasive computing systems, prototypes serve several uses and have different requirements related to those uses. We've developed CogTool to enable low-cost, rapid construction of interactive prototypes that serve all three UI purposes. CogTools core prototyping technique is storyboarding -specifically, interactive storyboarding using HTML. Rather than covering all possible pervasive systems, CogTool focuses on systems involving deliberate commands that the user invokes by some motor action. Such systems include PDAs, cell phones, handheld terminals (such as those used by rental car return personnel), in-vehicle driver information systems, and certain wearable computers that run desktop- or PDA-like applications.     

Bond computing systems: a biologically inspired and high-level dynamics model for pervasive computing

Targeting at modeling the high-level dynamics of pervasive computing systems, we introduce bond computing systems (BCS) consisting of objects, bonds and rules. Objects are typed but addressless representations of physical or logical (computing and communicating) entities. Bonds are typed multisets of objects. In a BCS, a configuration is specified by a multiset of bonds, called a collection. Rules specify how a collection evolves to a new one. A BCS is a variation of a P system introduced by Gheorghe Paun where, roughly, there is no maximal parallelism but with typed and unbounded number of membranes, and hence, our model is also biologically inspired. In this paper, we focus on regular bond computing systems (RBCS), where bond types are regular, and study their computation power and verification problems. Among other results, we show that the computing power of RBCS lies between linearly bounded automata (LBA) and LBC (a form of bounded multicounter machines) and hence, the regular bond-type reachability problem (given an RBCS, whether there is some initial collection that can reach some collection containing a bond of a given regular type) is undecidable. We also study a restricted model (namely, B-boundedness) of RBCS where the reachability problem becomes decidable.     

Linking Bayesian networks and PLS path modeling for causal analysis

Causal knowledge based on causal analysis can advance the quality of decision-making and thereby facilitate a process of transforming strategic objectives into effective actions. Several creditable studies have emphasized the usefulness of causal analysis techniques. Partial least squares (PLS) path modeling is one of several popular causal analysis techniques. However, one difficulty often faced when we commence research is that the causal direction is unknown due to the lack of background knowledge. To solve this difficulty, this paper proposes a method that links the Bayesian network and PLS path modeling for causal analysis. An empirical study is presented to illustrate the application of the proposed method. Based on the findings of this study, conclusions and implications for management are discussed.     

Verification of reactive systems using temporal logic with clocks

This paper presents a framework for the specification and verification of timing properties of reactive systems using Temporal Logic with Clocks (TLC). Reactive systems usually contain a number of parallel processes, therefore, it is essential to study and analyse each process based on its own local time. TLC is a temporal logic extended with multiple clocks, and it is in particular suitable for the specification of reactive systems. In our framework, the behavior of a reactive system is described through a formal specification; its timing properties, including safety and liveness properties, are expressed by TLC formulas. We also propose several demonstration techniques, such as an application of local reasoning and deriving fixed-time rules from the proof system of TLC, for proving that a reactive system meets its temporal specification. Under the proposed framework, the timing properties of a reactive system can therefore be directly reasoned about from the formal specification of the system.     

普适计算中一种最优服务选择算法的设计与仿真*

详细分析了服务选择问题及其求解目标,综合服务提供方高效率低成本和终端用户方的服务质量（QoS）等目标约束条件,提出一种多目标约束的最优服务选择遗传算法。该算法采用矩阵描述服务提供方、服务、终端用户三者之间的关系,并采用矩阵编码方式,将矩阵视为染色体个体,将矩阵的列视为染色体基因。仿真实验结果表明,该算法具有较好的收敛性和稳定的寻优能力。     

A simulation model for localization of pervasive objects using heterogeneous wireless networks

Position represents a relevant attribute needed by many applications, whose contexts are characterized by pervasiveness of the objects/things in the considered scenarios. In order to infer positions of pervasive objects, which are neither equipped with any location-sensing technologies, nor are unable to locate themselves, it is needed to support them with an appropriate infrastructure, which allows to determine their position in a manner that is transparent to applications. In this work, we aim at extending the positioning service using an agent-based approach, in order to discover and localize different kinds of objects, exploiting cheap and embedded technologies. We describe the design and the implementation of a layered architecture, that supports the localization of devices, and simple pervasive and ubiquitous objects. A simulation tool has been develop to evaluate the proposed solution in different application scenarios of every-day life.     

普适计算中的无缝迁移策略

针对分布式计算环境已有的一些迁移机制,都无法满足普适计算模式下任务迁移时对无缝性的要求,研究了任务的形式化描述,Agent的分类以及任务的迁移粒度问题.基于MobileAgent的任务无缝迁移策略,解决了迁移过程中的迁移算法、迁移时延、迁移失效等问题.其特点在于基于合理的迁移粒度和更小的迁移时延,通过MobileAgent的移动保证迁移的无缝性.多个应用场景中的测试实践表明了该策略的有效性.     

Situvis: A sensor data analysis and abstraction tool for pervasive computing systems

Pervasive systems are large-scale systems consisting of many sensors capturing numerous types of information. As this data is highly voluminous and dimensional, data analysis tasks can be extremely cumbersome and time-consuming. Enabling computers to recognise real-world situations is an even more difficult problem, involving not only data analysis, but also consistency checking. Here we present Situvis, an interactive visualisation tool for representing sensor data and creating higher-level abstractions from the data. This paper builds on previous work, Clear et al. (2009) [8] through evolved tool functionality and an evaluation of Situvis. A user-trial consisting of 10 participants shows that Situvis can be used to complete the key tasks in the development process of situation specifications in over 50% less time than an improvised alternative toolset.     

Failure diagnosis of discrete-event systems with linear-time temporal logic specifications

The paper studies failure diagnosis of discrete-event systems (DESs) with linear-time temporal logic (LTL) specifications. The LTL formulas are used for specifying failures in the system. The LTL-based specifications make the specification specifying process easier and more user-friendly than the formal language/automata-based specifications; and they can capture the failures representing the violation of both liveness and safety properties, whereas the prior formal language/automaton-based specifications can capture the failures representing the violation of only the safety properties (such as the occurrence of a faulty event or the arrival at a failed state). Prediagnosability and diagnosability of DESs in the temporal logic setting are defined. The problem of testing prediagnosability and diagnosability is reduced to the problem of model checking. An algorithm for the test of prediagnosability and diagnosability, and the synthesis of a diagnoser is obtained. The complexity of the algorithm is exponential in the length of each specification LTL formula, and polynomial in the number of system states and the number of specifications. The requirement of nonexistence of unobservable cycles in the system, which is needed for the diagnosis algorithms in prior methods to work, is relaxed. Finally, a simple example is given for illustration.     

Dynamic event-triggered prescribed performance control for nonlinear systems with signal temporal logic

This article is concerned with the problem of dynamic event-triggered prescribed performance control for nonlinear systems under signal temporal logic tasks. By utilizing the method of prescribed performance control, the constrained plant can be transformed into an unconstrained one, and a dynamic event-triggered feedback control law is generated for the transformed system to ensure that the signal temporal logic specification is satisfied. A dynamic event-triggered mechanism is designed to guarantee the event-triggered stability, safety and complex specification. Besides, Zeno phenomenon is definitely avoided. Compared with the continuous-time feedback controller, the event-triggered controller has proven to be effective in reducing sensing, communication and computation costs. Finally, two simulations are given to illustrate the effectiveness of theoretical results.     

Connecting the physical world with pervasive networks

This article addresses the challenges and opportunities of instrumenting the physical world with pervasive networks of sensor-rich, embedded computation. The authors present a taxonomy of emerging systems and outline the enabling technological developments.     

A complete coalition logic of temporal knowledge for multi-agent systems

Coalition logic (CL) is one of the most influential logical formalisms for strategic abilities of multi-agent systems. CL can specify what a group of agents can achieve through choices of their actions, denoted by [C]? to state that a group of agents C can have a strategy to bring about ? by collective actions, no matter what the other agents do. However, CL lacks the temporal dimension and thus can not capture the dynamic aspects of a system. Therefore, CL can not formalize the evolvement of rational mental attitudes of the agents such as knowledge, which has been shown to be very useful in specifications and verifications of distributed systems, and has received substantial amount of studies. In this paper, we introduce coalition logic of temporal knowledge (CLTK), by incorporating a temporal logic of knowledge (Halpern and Vardi’s logic of CKL _n ) into CL to equip CL with the power to formalize how agents’ knowledge (individual or group knowledge) evolves over the time by coalitional forces and the temporal properties of strategic abilities as well. Furthermore, we provide an axiomatic system for CLTK and prove that it is sound and complete, along with the complexity of the satisfiability problem which is shown to be EXPTIME-complete.