Actor languages their syntax, semantics, translation, and equivalence

In this paper we present two actor languages and a semantics preserving translation between them. The source of the translation is a high-level language that provides object-based programming abstractions. The target is a simple functional language extended with basic primitives for actor computation. The semantics preserved is the interaction semantics of actor systems — sets of possible interactions of a system with its environment. The proof itself is of interest since it demonstrates a methodology based on the actor theory framework for reasoning about correctness of transformations and translations of actor programs and languages and more generally of concurrent object languages.     

一个并发对象演算

由于缺乏一个为人们接受的描述并发对象系统语义的形式化模型,开发面向对象程序设计语言的开发受到了很大的制约,为了给并发面向对象程序设计定义一个公共的语义框架,人们分别以π演算和ａｃｔｏｒ模型为基础进行了研究。     

Asynchronous communication model based on linear logic

We propose a new framework called ACL for concurrent computation based on linear logic. ACL is a kind oflinear logic programming framework, where its operational semantics is described in terms ofproof construction in linear logic. We also give a model-theoretic semantics based onphase semantics, a model of linear logic. Our framework well captures concurrent computation based on asynchronous communication. It will, therefore, provide us with a new insight into other models of asynchronous concurrent computation from alogical point of view. We also expect ACL to become a formal framework for analysis, synthesis and transformation of concurrent programs by the use of techniques for traditional logic programming. ACL's attractive features for concurrent programming paradigms are also discussed.     

Revisiting actor programming in C++

The actor model of computation has gained significant popularity over the last decade. Its high level of abstraction makes it appealing for concurrent applications in parallel and distributed systems. However, designing a real-world actor framework that subsumes full scalability, strong reliability, and high resource efficiency requires many conceptual and algorithmic additives to the original model.In this paper, we report on designing and building CAF, the C++ Actor Framework. CAF targets at providing a concurrent and distributed native environment for scaling up to very large, high-performance applications, and equally well down to small constrained systems. We present the key specifications and design concepts—in particular a message-transparent architecture, type-safe message interfaces, and pattern matching facilities—that make native actors a viable approach for many robust, elastic, and highly distributed developments. We demonstrate the feasibility of CAF in three scenarios: first for elastic, upscaling environments, second for including heterogeneous hardware like GPUs, and third for distributed runtime systems. Extensive performance evaluations indicate ideal runtime at very low memory footprint for up to 64 CPU cores, or when offloading work to a GPU. In these tests, CAF continuously outperforms the competing actor environments Erlang, Charm++, SalsaLite, Scala, ActorFoundry, and even the raw message passing framework OpenMPI.     

一个计算机生成角色的行进避障算法

文章对计算机生成角色在分布式虚拟环境中行进时的障碍规避进行了研究。避障是计算机生成角色在行进中对各种障碍物的实时处理过程,文中给出了一个计算机生成角色的避障算法,对虚拟环境中不同类型的实体发生的可能碰撞采取了不同的避撞策略,着重研究了多个计算机生成角色间避障的方法;与已有的一些研究不同,笔者提出了可能障碍区和可能障碍集的概念,在此基础上对多个计算机生成角色产生可能障碍区后进行了实时处理;文中还给出了算法的正确性证明和时间复杂度分析。使用这个算法,可使计算机生成角色在虚拟环境中的行进行为更加逼真。     

Clustering of wireless sensor and actor networks based on sensor distribution and connectivity

Wireless Sensor and Actor Networks (WSANs) employ significantly more capable actor nodes that can collect data from sensors and perform application specific actions. To take these actions collaboratively at any spot in the monitored regions, maximal actor coverage along with inter-actor connectivity is desirable. In this paper, we propose a distributed actor positioning and clustering algorithm which employs actors as cluster-heads and places them in such a way that the coverage of actors is maximized and the data gathering and acting times are minimized. Such placement of actors is done by determining the k-hop Independent Dominating Set (IDS) of the underlying sensor network. Basically, before the actors are placed, the sensors pick the cluster-heads based on IDS. The actors are then placed at the locations of such cluster-heads. We further derive conditions to guarantee inter-actor connectivity after the clustering is performed. If inter-connectivity does not exist, the actors coordinate through the underlying sensors in their clusters to adjust their locations so that connectivity can be established. The performances of the proposed approaches are validated through simulations.     

Normative requirements for regulatory compliance: An abstract formal framework

By definition, regulatory rules (in legal context called norms) intend to achieve specific behaviour from business processes, and might be relevant to the whole or part of a business process. They can impose conditions on different aspects of process models, e.g., control-flow, data and resources etc. Based on the rules sets, norms can be classified into various classes and sub-classes according to their effects. This paper presents an abstract framework consisting of a list of norms and a generic compliance checking approach on the idea of (possible) execution of processes. The proposed framework is independent of any existing formalism, and provides a conceptually rich and exhaustive ontology and semantics of norms needed for business process compliance checking. Apart from the other uses, the proposed framework can be used to compare different compliance management frameworks (CMFs).     

Domains: Sharing state in the communicating event-loop actor model

The actor model is a message-passing concurrency model that avoids deadlocks and low-level data races by construction. This facilitates concurrent programming, especially in the context of complex interactive applications where modularity, security and fault-tolerance are required. The tradeoff is that the actor model sacrifices expressiveness and safety guarantees with respect to parallel access to shared state.In this paper we present domains as a set of novel language abstractions for safely encapsulating and sharing state within the actor model. We introduce four types of domains, namely immutable, isolated, observable and shared domains that each is tailored to a certain access pattern on that shared state. The domains are characterized with an operational semantics. For each we discuss how the actor model׳s safety guarantees are upheld even in the presence of conceptually shared state. Furthermore, the proposed language abstractions are evaluated with a case study in Scala comparing them to other synchronization mechanisms to demonstrate their benefits in deadlock freedom, parallel reads, and enforced isolation.     

A timed semantics of Orc

Orc is a kernel language for structured concurrent programming. Orc provides three powerful combinators that define the structure of a concurrent computation. These combinators support sequential and concurrent execution, and concurrent execution with blocking and termination.Orc is particularly well-suited for task orchestration, a form of concurrent programming with applications in workflow, business process management, and web service orchestration. Orc provides constructs to orchestrate the concurrent invocation of services while managing time-outs, priorities, and failures of services or communication.Our previous work on the semantics of Orc focused on its asynchronous behavior. The inclusion of time or the effect of delay on a computation had not been modeled. In this paper, we define an operational semantics of Orc that allows reasoning about delays, which are introduced explicitly by time-based constructs or implicitly by network delays. We develop a number of identities among Orc expressions and define an equality relation that is a congruence. We also present a denotational semantics in which the meaning of an Orc program is a set of traces, and show that the two semantics are equivalent.     

Automatically Detecting and Visualising Errors in UML Diagrams

UML has become the de facto standard for object-oriented modelling. Currently, UML comprises several different notations with no formal semantics attached to the individual diagrams or their integration, thus preventing rigorous analysis of the diagrams. Previously, we developed a formalisation framework that attaches formal semantics to a subset of UML diagrams used to model embedded systems. This paper describes automated structural and behavioural analyses applicable to UML diagrams using our formalisation framework. In addition to intra- and inter-diagram consistency checks, we discuss how simulation and model checking can be used in tandem for behavioural analysis of the UML diagrams. Our tools also visually interpret the analysis results in terms of the original UML diagrams, thereby facilitating their correction and refinement. We illustrate these capabilities through the modelling and analysis of UML diagrams for an automotive industrial case study. Correspondence and offprint requests to: Dr B. Cheng, Software Engineering and Network Systems Laboratory, Department of Computer Science and Engineering, Michigan State University, 3115 Engineering Building, East Lansing, MI 48824, USA. Tel.: +1 517 355 8344; Fax: +1 517 432 1061; Email: chengb@cse.msu.edu     

Semi-quantitative actor-based modelling as a tool to assess the drivers of change and physical variables in participatory integrated assessments

Integrated assessments that aim to support sustainable natural resources management require analysing how biophysical systems are impacted by human actions. These analyses are often performed by modelling the physical system, while human actions are prescribed as scenarios and introduced into the physical models by varying the model input. To achieve a more thorough analysis of the human system component in participatory integrated assessments, we developed a semi-quantitative approach for actor-based modelling which focuses on modelling actions of societal actors based on their problem perceptions but also computes the resulting changes of physical system variables. Our approach is intended to support transdisciplinary research and identification of sustainable development options in problem fields with high levels of uncertainty or ignorance, together with the actors that are being modelled. Actor-based modelling is done using an enhanced version of the DANA software. DANA allows modelling the actors in a specific problem field by representing the perception of each actor by directed graphs, and by computing optimal actions from the perspective of each actor. These perception graphs are semi-quantitative causal maps, which can easily be discussed among stakeholders in a participatory process. DANA was extended to support, in addition to actor modelling, the other two steps in actor-based modelling, modelling of actions and modelling of factors. Modelling of actions refers to determining the actions of each actor under certain scenario assumptions, taking into account the diverse problem perceptions of the individual actors in the problem field, the action of the other actors and exogenous changes. Modelling of factors refers to calculating, in a semi-quantitative way, the resulting changes of physical variables (e.g. pollutant emissions), which may serve as input to physical models. We applied actor-based modelling in an integrated assessment of mobile organic xenobiotics in rivers. Our study shows that actor-based modelling allows generating scientifically better founded and more transparent scenarios of the drivers of change in integrated assessments, in particular because they are based on a structured analysis of the actors' problem perceptions.     

Process Algebra Having Inherent Choice: Revised Semantics for Concurrent Systems

Process algebras are standard formalisms for compositionally describing systems by the dependencies of their observable synchronous communication. In concurrent systems, parallel composition introduces resolvable nondeterminism, i.e., nondeterminism that will be resolved in later design phases or by the operating system. Sometimes it is also important to express inherent nondeterminism for equal (communication) labels.Here, we give operational and axiomatic semantics to a process algebra having a parallel operator interpreted as concurrent and having a choice operator interpreted as inherent, not only w.r.t. different, but also w.r.t. equal next-step actions. In order to handle the different kinds of nondeterminism, the operational semantics uses μ-automata as underlying semantical model. Soundness and completeness of our axiom system w.r.t. the operational semantics is shown.     

A study of aboutness in information retrieval

This paper addresses the notion of aboutness in information retrieval. First, an exposition is given on how aboutness relates to relevance—a fundamental notion in information retrieval. A short summary is given on how aboutness is defined in more prominent information retrieval models. A model-theoretic definition of aboutness is then analyzed in an abstract setting using so called information fields. These allows properties of aboutness to be expressed independent of any given information retrieval model. As a consequence, information retrieval models can be theoretically compared according to what aboutness postulates they support. The Boolean and Coordinate retrieval models are compared in this fashion. In addition to model-theoretic aboutness, preferential entailment and conditional probabilities are employed to define aboutness between primitive information carriers. The preferential entailment approach is based on a preference semantics derived from nonmonotonic logics. The nonmonotonic behaviour of aboutness under information composition is highlighted. Rules describing how aboutness may be preserved under composition are proposed. Finally, a term aboutness definition drawn from a network-based probabilistic framework is analyzed. Conclusions regarding the implied retrieval effectiveness are drawn.     

Viewing control structures as patterns of passing messages

The purpose of this paper is to discuss some organizational aspects of programs using the actor model of computation. In this paper we present an approach to modelling intelligence in terms of a society of communicating knowledge-based problem-solving experts. In turn each of the experts can be viewed as a society that can be further decomposed in the same way until the primitive actors of the system are reached. We are investigating the nature of the communication mechanisms needed for effective problem-solving by a society of experts and the conventions of civilized discourse that make this possible. In this way we hope eventually to develop a framework adequate for the discussion of the central issues of problem-solving involving parallel versus serial processing and centralization versus decentralization of control and information storage.This paper demonstrates how actor message passing can be used to understand control structures as patterns of passing messages in serial processing. This paper is a pre-requisite for successors which treat issues of parallelism and communication within the framework established here. The ability to analyze or synthesize any kind of control structure as a pattern of passing messages among the members of a society provides an important tool for understanding control structures. Ultimately, we hope to be able to characterize various control structures in common use by societies in terms of patterns of passing messages. This paper makes a small step in this direction by showing how to characterize familiar control structures such as iteration and recursion in these terms.     

Consistency-based and abductive diagnoses as generalised stable models

If realistic systems are to be successfully modelled and efficiently diagnosed using model-based techniques, a more expressive language than classical logic is required. In this paper, we present a definition of diagnosis which allows the use of a nonmonotonic construct, negation as failure, in the modelling language. This definition is based on thegeneralised stable model semantics of abduction. Furthermore, we argue that, if negation as failure is permitted in the modelling language, the distinction between abductive and consistency-based diagnosis is no longer clear. Our definition allows both forms of diagnosis to be expressed in a single framework. It also allows a single interference procedure to perform abductive or consistency-based diagnosis, as appropriate.This paper is an extended and revised version of ref. [29].     

I-ABM: combining institutional frameworks and agent-based modelling for the design of enforcement policies

Computer science advocates institutional frameworks as an effective tool for modelling policies and reasoning about their interplay. In practice, the rules or policies, of which the institutional framework consists, are often specified using a formal language, which allows for the full verification and validation of the framework (e.g. the consistency of policies) and the interplay between the policies and actors (e.g. violations). However, when modelling large-scale realistic systems, with numerous decision-making entities, scalability and complexity issues arise making it possible only to verify certain portions of the problem without reducing the scale. In the social sciences, agent-based modelling is a popular tool for analysing how entities interact within a system and react to the system properties. Agent-based modelling allows the specification of complex decision-making entities and experimentation with large numbers of different parameter sets for these entities in order to explore their effects on overall system performance. In this paper we describe how to achieve the best of both worlds, namely verification of a formal specification combined with the testing of large-scale systems with numerous different actor configurations. Hence, we offer an approach that allows for reasoning about policies, policy making and their consequences on a more comprehensive level than has been possible to date. We present the institutional agent-based model methodology to combine institutional frameworks with agent-based simulations). We furthermore present J-InstAL, a prototypical implementation of this methodology using the InstAL institutional framework whose specifications can be translated into a computational model under the answer set semantics, and an agent-based simulation based on the jason tool. Using a simplified contract enforcement example, we demonstrate the functionalities of this prototype and show how it can help to assess an appropriate fine level in case of contract violations.     

A Rewriting Logic Approach to Operational Semantics (Extended Abstract)

This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, and continuation-based semantics. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.