This paper introduces *distributed speculative inference (DSI)*, a novel inference algorithm that is provably faster than speculative inference (SI) [leviathan2023, chen2023, miao2024, sun2025, timor2025] and standard autoregressive inference (non-SI). Like other SI algorithms, DSI operates on frozen language models (LMs), requiring no training or architectural modifications, and it preserves the target distribution. Prior studies on SI have demonstrated empirical speedups over non-SI—but rely on sufficiently fast and accurate drafters, which are often unavailable in practice. We identify a gap where SI can be slower than non-SI if drafters are too slow or inaccurate. We close this gap by proving that DSI is faster than both SI and non-SI—given any drafters. DSI is therefore not only faster than SI, but also unlocks the acceleration of LMs for which SI fails. DSI leverages *speculation parallelism (SP)*, a novel type of task parallelism, to orchestrate target and drafter instances that overlap in time, establishing a new foundational tradeoff between computational resources and latency. Our simulations show that DSI is 1.29-1.92x faster than SI in single-node setups for various off-the-shelf LMs and tasks. We open-source all our code.

Accelerating the inference of large language models (LLMs) is a critical challenge in generative AI. Speculative decoding (SD) methods offer substantial efficiency gains by generating multiple tokens using a single target forward pass. However, existing SD approaches require the drafter and target models to share the same vocabulary, thus limiting the pool of possible drafters, often necessitating the training of a drafter from scratch. We present three new SD methods that remove this shared-vocabulary constraint. All three methods preserve the target distribution (i.e., they are lossless) and work with off-the-shelf models without requiring additional training or modifications. Empirically, on summarization, programming, and long-context tasks, our algorithms demonstrate significant speedups of up to 2.8x over standard autoregressive decoding. By enabling any off-the-shelf model to serve as a drafter and requiring no retraining, this work substantially broadens the applicability of the SD framework in practice.

System and Software Engineering is about implementing “what the user wanted” (colloquial phrasing borrowed from the famous tree-swing cartoon; seeFig. 1). We begin this paper by revisiting briefly the decades-long continuous pursuit of answers to some of the underlying engineering challenges, carried out by the first-listed author and his colleagues. Along this road, concepts like executable specifications, visual formalisms, hierarchies, abstractions, and scenarios play major roles. We then reflect upon the observation that the very discovery of “what the user wanted,” which often appears to require only elicitation in some structured requirement engineering process, actually poses significant challenges of its own. Documenting in advance the requirements for a real-world reactive system, such as an autonomous vehicle—and more generally, producing a textual and visual description of what a system does or needs to do—is becoming ever harder, and in certain cases impossible. Furthermore, producing quality specifications is critical not only for eventually satisfying the user, but for early detection of critical faults. We conclude by outlining future approaches and tools that may be able to mitigate the severity of this issue.

Abstract Deep reinforcement learning (DRL) has become a dominant deep-learning paradigm for tasks where complex policies are learned within reactive systems. Unfortunately, these policies are known to be susceptible to bugs. Despite significant progress in DNN verification, there has been little work demonstrating the use of modern verification tools on real-world, DRL-controlled systems. In this case study, we attempt to begin bridging this gap, and focus on the important task of mapless robotic navigation — a classic robotics problem, in which a robot, usually controlled by a DRL agent, needs to efficiently and safely navigate through an unknown arena towards a target. We demonstrate how modern verification engines can be used for effective model selection , i.e., selecting the best available policy for the robot in question from a pool of candidate policies. Specifically, we use verification to detect and rule out policies that may demonstrate suboptimal behavior, such as collisions and infinite loops. We also apply verification to identify models with overly conservative behavior, thus allowing users to choose superior policies, which might be better at finding shorter paths to a target. To validate our work, we conducted extensive experiments on an actual robot, and confirmed that the suboptimal policies detected by our method were indeed flawed. We also demonstrate the superiority of our verification-driven approach over state-of-the-art, gradient attacks. Our work is the first to establish the usefulness of DNN verification in identifying and filtering out suboptimal DRL policies in real-world robots, and we believe that the methods presented here are applicable to a wide range of systems that incorporate deep-learning-based agents.

Autonomous systems emerge from the need to progressively replace human operators by autonomous agents in a wide variety of application areas. We offer an analysis of the state of the art in developing autonomous systems, focusing on design and validation and showing that the multi-faceted challenges involved go well beyond the limits of weak AI. We argue that traditional model-based techniques are defeated by the complexity of the problem, while solutions based on end-to-end machine learning fail to provide the necessary trustworthiness. We advocate a hybrid design approach, which combines the two, adopting the best of each, and seeks tradeoffs between trustworthiness and performance. We claim that traditional risk analysis and mitigation techniques fail to scale and discuss the trend of moving away from correctness at design time and toward reliance on runtime assurance techniques. We argue that simulation and testing remain the only realistic approach for global validation and show how current methods can be adapted to autonomous systems. We conclude by discussing the factors that will play a decisive role in the acceptance of autonomous systems and by highlighting the urgent need for new theoretical foundations.

Artificial intelligence (AI) techniques, including, e.g., machine learning, multi-agent collaboration, planning, and heuristic search, are emerging as ever-stronger tools for solving hard problems in real-world applications. Executable specification techniques (ES), including, e.g., Statecharts and scenario-based programming, is a promising development approach, offering intuitiveness, ease of enhancement, compositionality, and amenability to formal analysis. We propose an approach for integrating AI and ES techniques in developing complex intelligent systems, which can greatly simplify agile/spiral development and maintenance processes. The approach calls for automated detection of whether certain goals and sub-goals are met; a clear division between sub-goals solved with AI and those solved with ES; compositional and incremental addition of AI-based or ES-based components, each focusing on a particular gap between a current capability and a well-stated goal; and, iterative refinement of sub-goals solved with AI into smaller sub-sub-goals where some are solved with ES, and some with AI. We describe the principles of the approach and its advantages, as well as key challenges and suggestions for how to tackle them.

We present a development environment that proactively and interactively assists the software engineer in modeling complex reactive systems. Our framework repeatedly analyzes models of the system under development at various levels of abstraction, and then reasons about these models in order to detect possible errors and to derive emergent properties of interest. Upon request, the environment can then augment the system model in order to repair or avoid detected behavior that is undesired, or instrument it in order to monitor the execution for certain behaviors. Specialized automated and human-assisted techniques are incorporated to direct and prioritize the analysis and related tasks, based on the relevance of the observed properties and the expected impact of actions to be taken. Our development environment is an initial step in the direction of the very recent Wise Computing vision, which calls for turning the computer (namely, the development environment) into an equal member of the development team: knowledgeable, independent, concerned and proactively involved in the development process. Our tool is implemented within the context of behavioral programming (BP), a scenario-based modeling approach, where components are aligned with how humans often describe desired system behavior. Thus, our work further enhances the naturalness and incrementality of developing in BP.

BACKGROUND: Research related to cancer is vast, and continues in earnest in many directions. Due to the complexity of cancer, a better understanding of tumor growth dynamics can be gleaned from a dynamic computational model. We present a comprehensive, fully executable, spatial and temporal 3D computational model of the development of a cancerous tumor together with its environment. RESULTS: The model was created using Statecharts, which were then connected to an interactive animation front-end that we developed especially for this work, making it possible to visualize on the fly the on-going events of the system's execution, as well as the effect of various input parameters. We were thus able to gain a better understanding of, e.g., how different amounts or thresholds of oxygen and VEGF (vascular endothelial growth factor) affect the progression of the tumor. We found that the tumor has a critical turning point, where it either dies or recovers. If minimum conditions are met at that time, it eventually develops into a full, active, growing tumor, regardless of the actual amount; otherwise it dies. CONCLUSIONS: This brings us to the conclusion that the tumor is in fact a very robust system: changing initial values of VEGF and oxygen can increase the time it takes to become fully developed, but will not necessarily completely eliminate it.

The ability to create succinct programs is a central criterion for comparing programming and specification methods. Specifically, approaches to concurrent programming can often be thought of as idioms for the composition of automata, and as such they can then be compared using the standard and natural measure for the complexity of automata, descriptive succinctness. This measure captures the size of the automata that the evaluated approach needs for expressing the languages under discussion. The significance of this metric lies, among other things, in its impact on software reliability, maintainability, reusability and simplicity, and on software analysis and verification. Here, we focus on the succinctness afforded by three basic concurrent programming idioms: requesting events, blocking events and waiting for events. We show that a programming model containing all three idioms is exponentially more succinct than non-parallel automata, and that its succinctness is additive to that of classical nondeterministic and "and" automata. We also show that our model is strictly contained in the model of cooperating automata à la statecharts, but that it may provide similar exponential succinctness over non-parallel automata as the more general model - while affording increased encapsulation. We then investigate the contribution of each of the three idioms to the descriptive succinctness of the model as a whole, and show that they each have their unique succinctness advantages that are not subsumed by their counterparts. Our results contribute to a rigorous basis for assessing the complexity of specifying, developing and maintaining complex concurrent software.

We present a method for the automatic compositional verification of certain classes of concurrent programs. Our approach is based on the casting of the model checking problem into a theory of transition systems within CVC4, a DPLL(T) based SMT solver. Our transition system theory then cooperates with other theories supported by the solver (e.g., arithmetic, arrays), which can help accelerate the verification process. More specifically, our theory solver looks for known patterns within the input programs and uses them to generate lemmas in the languages of other theories. When applicable, these lemmas can often steer the search away from safe parts of the search space, reducing the number of states to be explored and expediting the model checking procedure. We demonstrate the potential of our technique on a number of broad classes of programs.

In recent years formal verification techniques have become an important part of the development cycle of concurrent software. In order to tackle the state explosion problem and verify larger systems, a great deal of work has been put into improving the scalability of verification tools. In this work, we seek to draw attention to an alternative/complementary approach to improving scalability, which sometimes receives less notice: the effect the concurrent programming model itself has on one’s ability to verify programs encoded within it. Recent work suggests that a suitable choice of model, tailored to the problem at hand, may render the produced software more amenable to verification techniques. We recapitulate some recent and new results demonstrating this effect in programming models for discrete, synchronous reactive systems, and outline some directions for future work. We hope that the paper will trigger additional research on this important topic.

We present a model for the automatic semantic analysis of requirements elicitation documents.Our target semantic representation employs live sequence charts, a multi-modal visual language for scenariobased programming, which can be directly translated into executable code.The architecture we propose integrates sentencelevel and discourse-level processing in a generative probabilistic framework for the analysis and disambiguation of individual sentences in context.We show empirically that the discourse-based model consistently outperforms the sentence-based model when constructing a system that reflects all the static (entities, properties) and dynamic (behavioral scenarios) requirements in the document.

In this article, we discuss the possible connection between the programming language and the paradigm behind it, and programmers’ tendency to adopt an external or internal perspective of the system they develop. Based on a qualitative analysis, we found that when working with the visual, interobject language of live sequence charts (LSC), programmers tend to adopt an external and usability-oriented view of the system, whereas when working with an intraobject language, they tend to adopt an internal and implementation-oriented viewpoint. This is explained by first discussing the possible effect of the programming paradigm on programmers’ perception and then offering a more comprehensive explanation. The latter is based on a cognitive model of programming with LSC, which is an interpretation and a projection of the model suggested by Adelson and Soloway [1985] onto LSC and scenario-based programming, the new paradigm on which LSC is based. Our model suggests that LSC fosters a kind of programming that enables iterative refinement of the artifact with fewer entries into the solution domain. Thus, the programmer can make less context switching between the solution domain and the problem domain, and consequently spend more time in the latter. We believe that these findings are interesting mainly in two ways. First, they characterize an aspect of problem-solving behavior that to the best of our knowledge has not been studied before—the programmer’s perspective. The perspective can potentially affect the outcome of the problem-solving process, such as by leading the programmer to focus on different parts of the problem. Second, relating the structure of the language to the change in perspective sheds light on one of the ways in which the programming language can affect the programmer’s behavior.

We present a method and a tool for composing a reactive system and for accompanying the development and documentation process with a proof of its correctness. The approach is based on behavioral programming (BP) and the Z3 SMT solver. We show how program verification can be automated and streamlined by combining properties of individual modules, specified and verified separately, with application-independent specifications both of the BP semantics and of general theories. The method may yield an exponential acceleration of the verification process when compared with model-checking the composite application. We show that formalization of properties of independent modules in preparation for the correctness proofs can be useful as documentation for future development. We view this work as a further step towards making formal correctness proofs standard practice in the development of reactive systems, and carried out by programmers at large.

We propose a framework for the development of switched fuzzy systems, in which the discrete characteristics of the mode-switching logic are implemented using the paradigm of behavioral programming: they are coded as independent behavior threads and are interwoven at runtime. We demonstrate how such mode switching enables the simplification of fuzzy rules, and reduces their total number, as well as the number of rules evaluated in a computation cycle. The ability of the behavioral programming approach to describe independent simultaneous aspects of behavior in a modular and incremental manner, which aligns with how people often specify requirements, is shown to complement the intuitive nature of fuzzy logic. Our approach is backed by a Java package that provides an initial infrastructure for implementations.

The talk will briefly describe three of Turing's major achievements, in three different fields: computability, biological modeling and artificial intelligence. Interspersed with this, I will explain how each of them directly motivated and inspired me to carry out a variety of research projects over a period of 30 years, the results of which can all be viewed humbly as extensions and generalizations of Turing's pioneering and ingenious insights.

In behavioral programming, scenarios are used to program the behavior of reactive systems. Behavioral programming originated in the language of live sequence charts (LSC), a visual formalism based on multi-modal scenarios, and supported by a mechanism for directly executing a system described by a set of LSCs. In an exploratory experiment, we compare programming using LSCs with procedural programming using Java, and seek the best interface for creating the visual artifact of LSCs. Several interfaces for creating LSCs were tested, among them a novel interactive natural language interface (NL). Our preliminary results indicate that even experts in procedural programming preferred the LSCs NL interface over the Java alternative, and their implementation times were comparable to those of the other interfaces tested. The results indicate that the NL interface, combined with the scenario-based essence of LSCs, may be a viable alternative to conventional programming.

The talk will survey the highlights of work carried out in the last 30 years, regarding visual languages for the programming of reactive systems. I'll discuss the intra-object language of statecharts and the inter-object language of live sequence charts (LSC) with its play-in interface, as well as a non-visual counterpart thereof, based on Java. Some recent work on a natural language interface for LSCs and its combination with play-in will also be shown.

In his pioneering 1952 paper, “The chemical basis of morphogenesis”, Alan Turing introduced, perhaps for the first time, a model of the morphogenesis of embryo development. Central to his theory is the concept of cells with chemical entities that int

System specifications are often structured as collections of scenarios and use-cases that describe desired and forbidden sequences of events. A recently proposed behavioral programming approach, which evolved from the visual language of live sequence charts (LSCs), calls for coding software modules in alignment with such scenarios. We present a methodology and a supporting model-checking tool for verifying behavioral Java programs, without having to first translate them into a specific input language for the model checker. Our method facilitates early discovery of conflicting or under-specified scenarios, which can often be resolved by adding new scenarios rather than by changing existing code. Also, counterexamples provided by the tool are themselves event sequences that can serve directly for refinements and corrections. Our tool reduces the size of the execution state-space using an abstraction that focuses on behaviorally interesting states and treats transitions between them as atomic.

We introduce a way to program adaptive reactive systems, using behavioral, scenario-based programming. Extending the semantics of live sequence charts with reinforcements allows the programmer not only to specify what the system should do or must not do, but also what it should try to do, in an intuitive and incremental way. By integrating scenario-based programs with reinforcement learning methods, the program can adapt to the environment, and try to achieve the desired goals. Visualization methods and modular learning decompositions, based on the unique structure of the program, are suggested, and result in an efficient development process and a fast learning rate.

We address the problem of comprehending cause and effect relationships between relatively independent behavior components of a single application. Our focus is on the paradigm of behavioral, scenario-based, programming, as captured by the language of live sequence charts (LSC) or its Java-based counterpart, BPJ. In this programming paradigm, multi-modal behaviors can be specified separately, and are integrated only at run time. We present a tool, with which the user can easily follow the decisions of the collective execution mechanism. It shows the behaviors and events that were executed at each point in time, and those that were delayed or abandoned, as well as the causes and reasons behind these run-time choices. The dynamic effects of such decisions on the system's behavior can be seen easily too.

We exploit the main similarity between the aspect-oriented programming paradigm and the inter-object, scenario-based approach to specification, in order to construct a new way of executing systems based on the latter. Specifically, we transform multimodal scenario-based specifications, given in the visual language of live sequence charts (LSC), into what we call scenario aspects , implemented in AspectJ. Unlike synthesis approaches, which attempt to take the inter-object scenarios and construct intra-object state-based per-object specifications or a single controller automaton, we follow the ideas behind the LSC play-out algorithm to coordinate the simultaneous monitoring and direct execution of the specified scenarios. Thus, the structure of the specification is reflected in the structure of the generated code; the high-level inter-object requirements and their structure are not lost in the translation. The transformation/compilation scheme is fully implemented in a UML2-compliant tool we term the S2A compiler (for Scenarios to Aspects), which provides full code generation of reactive behavior from inter-object multimodal scenarios. S2A supports advanced scenario-based programming features, such as multiple instances and exact and symbolic parameters. We demonstrate our work with an application whose inter-object behaviors are specified using LSCs. We discuss advantages and challenges of the compilation scheme in the context of the more general vision of scenario-based programming.

We present PlayGo, a comprehensive tool for scenario-based programming, built around the language of live sequence charts and the play-in/play-out approach [7], which includes a compiler into AspectJ code and means for debugging the execution. PlayGo is intended to be a full IDE that addresses major parts of the vision of Liberating Programming [3]. This paper presents the first version of PlayGo, which already includes several of the intended capabilities.

The following topics are dealt with: finite model theory; logic and automata; semantics; process calculi; and coalgebras.

The scenario-based approach to specification and programming uses powerful extensions of sequence diagrams, such as LSCs (live sequence charts), to model system behavior. Previous work in this area presents interesting challenges related to the scalability of the approach and to better tool support for analysis, execution, and comprehension. Here we suggest new semantic-rich ways of viewing sequence diagrams and LSCs for better comprehension of both a single large chart and a full multi-chart specification, in a variety of software engineering tasks. Our method uses weighted messages to create a semantic order that enables semantic zooming and scrolling of different parts of a chart, providing visual hints about context.

Most of this piece focuses on Amir's personality, since FACS readers are unlikely to need too much introduction to his scientific contributions.Amir completed his PhD in applied mathematics, the tile of his thesis being Calculation of Tides in the Ocean, under Chaim Pekeris, who was the founder of our department at the Weizmann Institute.He then switched to computer science during a brief stint at Stanford and at IBM Yorktown Heights.He was then at the Weizmann Institute until 1973, with two other young, brilliant computer scientists: Shimon Even and Zohar Manna.The three of them left Weizmann within a year of each other, each one for a completely different reason.Amir went to

Complex biological systems involve incorporated behaviors of numerous processes, mechanisms and objects. However, experimental analysis, by its nature, divides biological systems into static interactions with little dynamics. To bridge the gap betwee

A primary goal for artificial nose (eNose) technology is to report perceptual qualities of novel odors. Currently, however, eNoses primarily detect and discriminate between odorants they previously "learned". We tuned an eNose to human odor pleasantness estimates. We then used the eNose to predict the pleasantness of novel odorants, and tested these predictions in naïve subjects who had not participated in the tuning procedure. We found that our apparatus generated odorant pleasantness ratings with above 80% similarity to average human ratings, and with above 90% accuracy at discriminating between categorically pleasant or unpleasant odorants. Similar results were obtained in two cultures, native Israeli and native Ethiopian, without retuning of the apparatus. These findings suggest that unlike in vision and audition, in olfaction there is a systematic predictable link between stimulus structure and stimulus pleasantness. This goes in contrast to the popular notion that odorant pleasantness is completely subjective, and may provide a new method for odor screening and environmental monitoring, as well as a critical building block for digital transmission of smell.

The talk shows the way techniques from computer science and software engineering can be applied beneficially to research in the life sciences. We will discuss the idea of comprehensive and realistic modeling of biological systems, where we try to understand and analyze an entire system in detail, utilizing in the modeling effort all that is known about it. I will address the motivation for such modeling and the philosophy underlying the techniques for carrying it out, as well as the crucial question of when such models are to be deemed valid, or complete. The examples I will present will be from among the biological modeling efforts my group has been involved in: T cell development in the thymus, lymph node behavior, organogenesis of the pancreas, fate determination in the reproductive system of C. elegans, and a generic cell model. The ultimate long-term “grand challenge” is to produce an interactive, dynamic, computerized model of an entire multi-cellular organism, such as the C. elegans nematode worm, which is complex, but well-defined in terms of anatomy and genetics. The challenge is to construct a full, true-to-all-known-facts, 4-dimensional, interactively animated model of the development and behavior of this worm (or of a comparable multi-cellular animal), which is easily extendable as new biological facts are discovered.

Lymph nodes are organs in which lymphocytes respond to antigens to generate, among other cell types, plasma cells that secrete specific antibodies and memory lymphocytes for enhanced future responses to the antigen. To achieve these ends, the lymph node (LN) has to orchestrate the meeting and interactions between the antigen and various cell types including the rare clones of B cells and T cells bearing receptors for the antigen. The process is dynamic in essence and involves chemotaxis of responding cells through various anatomical compartments of the LN and selective cell differentiation, proliferation and programmed death. Understanding the LN requires a dynamic integration of the mass of data generated by extensive experimentation. Here, we present a fully executable, bottom-up computerized model of the LN using the visual language of Statecharts and the technology of reactive animation (RA) to create a dynamic front-end. We studied the effects of amount of antigen and LN size on the emergent properties of lymphocyte dynamics, differentiation and anatomic localization. The dynamic organization of the LN visualized by RA sheds new light on how the immune system transforms antigen stimulation into a highly sensitive, yet buffered response.

Although the family of genes encoding for olfactory receptors was identified more than 15 years ago, the difficulty of functionally expressing these receptors in an heterologous system has, with only some exceptions, rendered the receptive range of given olfactory receptors largely unknown. Furthermore, even when successfully expressed, the task of probing such a receptor with thousands of odors/ligands remains daunting. Here we provide proof of concept for a solution to this problem. Using computational methods, we tune an electronic nose to the receptive range of an olfactory receptor. We then use this electronic nose to predict the receptors' response to other odorants. Our method can be used to identify the receptive range of olfactory receptors, and can also be applied to other questions involving receptor-ligand interactions in non-olfactory settings.

The last several decades have witnessed a vast accumulation of biological data and data analysis. Many of these data sets represent only a small fraction of the system's behavior, making the visualization of full system behavior difficult. A more complete understanding of a biological system is gained when different types of data (and/or conclusions drawn from the data) are integrated into a larger-scale representation or model of the system. Ideally, this type of model is consistent with all available data about the system, and it is then used to generate additional hypotheses to be tested. Computer-based methods intended to formulate models that integrate various events and to test the consistency of these models with respect to the laboratory-based observations on which they are based are potentially very useful. In addition, in contrast to informal models, the consistency of such formal computer-based models with laboratory data can be tested rigorously by methods of formal verification. We combined two formal modeling approaches in computer science that were originally developed for non-biological system design. One is the inter-object approach using the language of live sequence charts (LSCs) with the Play-Engine tool, and the other is the intra-object approach using the language of statecharts and Rhapsody as the tool. Integration is carried out using InterPlay, a simulation engine coordinator. Using these tools, we constructed a combined model comprising three modules. One module represents the early lineage of the somatic gonad of C. elegans in LSCs, while a second more detailed module in statecharts represents an interaction between two cells within this lineage that determine their developmental outcome. Using the advantages of the tools, we created a third module representing a set of key experimental data using LSCs. We tested the combined statechart-LSC model by showing that the simulations were consistent with the set of experimental LSCs. This small-scale modular example demonstrates the potential for using similar approaches for verification by exhaustive testing of models by LSCs. It also shows the advantages of these approaches for modeling biology.

In this paper - as a natural extension of the idea of using visual formalisms for the modeling itself - we present a technique for the visualization and exploration of execution traces of such models. Our approach is different from previous approaches, most of which consider execution traces at the code level, look for interaction patterns in the traces, or generate concrete sequence diagrams from recorded execution traces. In contrast, we take an inter-object scenario-based behavioral model given by the designer as input, and visualize the activation and progress of the scenarios therein as they "come to life" during execution. We illustrate the ideas using modal scenarios, given in a UML-compliant dialect of live sequence charts (LSC).

Experiments have generated a plethora of data about the genes, molecules, and cells involved in thymocyte development. Here, we use a computer-driven simulation that uses data about thymocyte development to generate an integrated dynamic representation-a novel technology we have termed reactive animation (RA). RA reveals emergent properties in complex dynamic biological systems. We apply RA to thymocyte development by reproducing and extending the effects of known gene knockouts: CXCR4 and CCR9. RA simulation revealed a previously unidentified role of thymocyte competition for major histocompatability complex presentation. We now report that such competition is required for normal anatomical compartmentalization, can influence the rate of thymocyte velocities within chemokine gradients, and can account for the disproportion between single-positive CD4 and CD8 lineages developing from double-positive precursors.

We exploit the main similarity between the aspect-oriented programming paradigm and the inter-object, scenario-based approach to specification in order to construct a new way of executing systems based on the latter. Specifically, we show how to compile multi-modal scenario-based specifications, given in the visual language of Live Sequence Charts (LSC), into what we call Scenario Aspects, implemented in AspectJ. Unlike synthesis approaches, which attempt to take the inter-object scenarios and construct intra-object state-based specifications, we follow the ideas behind the LSC play-out algorithm to coordinate the simultaneous monitoring and direct execution of the specified scenarios. We demonstrate our compilation scheme using a small application whose inter-object behaviors are specified using LSCs.

We describe InterPlay, a simulation engine coordinator that supports cooperation and interaction of multiple simulation and execution tools, thus helping to scale up the design and development cycle of reactive systems. InterPlay involves a number of related ideas. In the first, we concentrate on the interobject design approach involving live sequence charts (LSCs) and its support tool, the play-engine, enabling multiple play-engines to run in cooperation. This makes possible the distributed design of large-scale systems by different teams, as well as the refinement of parts of a system using different play-engines. The second idea concerns combining the interobject approach with the more conventional intraobject approach, involving, for example, statecharts and Rhapsody. InterPlay makes it possible to run the play-engine in cooperation with Rhapsody, and is very useful when some system objects have clear and distinct internal behavior, or in an iterative development process where the design is implementation-oriented and the ultimate goal is to end up with an intraobject implementation. Finally, we have expanded the play-engine's ability to delegate some of the system's functionality to complex GUIs. This enables beneficial interaction with "smart" GUIs that have built-in behavior of their own, and which are more naturally implemented in code

We present an algorithm for drawing directed graphs which is based on rapidly solving a unique one-dimensional optimization problem for each of the axes. The algorithm results in a clear description of the hierarchy structure of the graph. Nodes are not restricted to lie on fixed horizontal layers, resulting in layouts that convey the symmetries of the graph very naturally. The algorithm can be applied without change to cyclic or acyclic digraphs and even to graphs containing both directed and undirected edges. We also derive a hierarchy index from the input digraph, which quantitatively measures its amount of hierarchy.

We describe a novel approach to the visualization of hierarchical clustering that superimposes the classical dendrogram over a fully synchronized low-dimensional embedding, thereby gaining the benefits of both approaches. In a single image one can view all the clusters, examine the relations between them and study many of their properties. The method is based on an algorithm for low-dimensional embedding of clustered data, with the property that separation between all clusters is guaranteed, regardless of their nature. In particular, the algorithm was designed to produce embeddings that strictly adhere to a given hierarchical clustering of the data, so that every two disjoint clusters in the hierarchy are drawn separately.

The vertices of most graphs that appear in real applications are nonuniform. They can be circles, ellipses, rectangles, or other geometric elements of varying shapes and sizes. Unfortunately, current force directed methods for laying out graphs are suitable mostly for graphs whose vertices are zero-sized and dimensionless points. It turns out that naively extending these methods to handle nonuniform vertices results in serious deficiencies in terms of output quality and performance. In this paper we try to remedy this situation by identifying the special characteristics and problematics of such graphs and offering several algorithms for tackling them. The algorithms can be viewed as carefully constructed extensions of force-directed methods, and their output quality and performance are similar.

Remarkable progress in various fields of biology is leading in the direction of a complete map of the building blocks of biological systems. There is broad agreement among researchers that 21st century biology will focus on attempting to understand how component parts collaborate to create a whole. It is also well agreed that this transition of biology from identifying the building blocks (analysis) to integrating the parts into a whole (synthesis) should rely on the language of mathematics. In a recent publication, we described the results of a first attempt at confronting the above challenge using the visual formalism of statecharts. We presented a detailed model for T cell activation using statecharts within the general framework of object-oriented modeling. In this work, we compare the statechart-based modeling approach to a Boolean formalism presented by Thomas & D'Ari. This comparison was done by taking a model for T cell activation and anergy, which was constructed by Kaufman et al. using such a Boolean formalism, and translating it into the language of statecharts. Comparing these two representations of the same phenomena allows us to assess the advantages and disadvantages of each modeling approach. We believe that the results of this work, together with the results of our previous modeling work on T cell activation, should encourage the use of visual formalisms such as statecharts for modeling complex biological systems.

We extend live sequence charts (LSCs), a highly expressive variant of sequence diagrams, and provide the extension with an executable semantics. The extension involves support for instances that can bind to multiple objects and symbolic variables that can bind to arbitrary values. The result is a powerful executable language for expressing behavioral requirements on the level of inter-object interaction. The extension is implemented in full in our play-engine tool, with which one can execute the requirements directly without the need to build or synthesize an intra-object system model. It seems that in addition to many advantages in testing and requirements engineering, for some kinds of systems this could lead to the requirements actually serving as the final implementation.

We consider state-based behavior in object-oriented analysis and design, as it arises, for example, in specifying behavior in the UML using statecharts. We first provide a rigorous and analyzable model of object systems and their reactivity. The definition is for basic one-thread systems, but can be extended in appropriate ways to more elaborate models. We then address the notion of inheritance and behavioral conformity and the resulting substitutability of classes, whereby inheriting should retain the system's original behaviors. Inheritance is a central issue of crucial importance to the modeling, design, and verification of object-oriented systems, and the many deep and unresolved questions around it cannot be addressed without a precise definition of the systems under consideration. We use our definition to give a clear and rigorous picture of what exactly is meant by behavioral conformity and how computationally complex it is to detect.

Discovering significant patterns that exist implicitly in huge spatial databases is an important computational task. A common approach to this problem is to use cluster analysis. We propose a novel approach to clustering, based on the deterministic analysis of random walks on a weighted graph generated from the data. Our approach can decompose the data into arbitrarily shaped clusters of different sizes and densities, overcoming noise and outliers that may blur the natural decomposition of the data. The method requires only O(n log n) time, and one of its variants needs only constant space.

We present a multi-scale layout algorithm for the aesthetic drawing of undirected graphs with straight-line edges. The algorithm is extremely fast, and is capable of drawing graphs of substantially larger size than any other algorithm we are awars of. For example, the algorithm achieves optimal drawings of 1000 vertex graphs in less than 3 seconds. The paper contains graphs with over 6000 nodes. The proposed algorithm embodies a new multi-scale scheme for drawing graphs, which can significantly improve the speed of essentially any force-directed method.

We present an algorithm for the aesthetic drawing of basic hierarchical blob structures, of the kind found in higraphs and statecharts and in other diagrams in which hierarchy is depicted as topological inclusion. Our work could also be useful in window system dynamics, and possibly also in things like newspaper layout, etc. Several criteria for aesthetics are formulated, and we discuss their motivation, our methods of implementation and the algorithm's performance.

The paper puts forward some thoughts on theoretical vs. applied research in the specification and design of reactive, highly concurrent systems. It discusses the calculus of communicating systems and communicating sequential processes.

This paper continues our work on infinite, recursive structures. We investigate the descriptive complexity of several logics over recursive structures, including first-order, second-order, and fixpoint logic, exhibiting connections between expressibility of a property and its computational complexity. We then address 0-1 laws, proposing a version that applies to recursive structures and using it to prove several non-expressibility results.

The paradigm of simulated annealing is applied to the problem of drawing graphs “nicely.” Our algorithm deals with general undirected graphs with straight-line edges, and employs several simple criteria for the aesthetic quality of the result. The algorithm is flexible, in that the relative weights of the criteria can be changed. For graphs of modest size it produces good results, competitive with those produced by other methods, notably, the “spring method” and its variants.

We describe the semantics of statecharts as implemented in the STATEMATE system. This was the first executable semantics defined for the language and has been in use for almost a decade. In terms of the controversy around whether changes made in a given step should take effect in the current step or in the next one, this semantics adopts the latter approach.

Article Will I be pretty, will I be rich?: some thoughts on theory vs. practice in systems engineering Share on Author: David Harel The Weizmann Institute of Science, Rehovot, Israel The Weizmann Institute of Science, Rehovot, IsraelView Profile Authors Info & Claims PODS '94: Proceedings of the thirteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systemsMay 1994 Pages 1–3https://doi.org/10.1145/182591.182592Published:24 May 1994 0citation145DownloadsMetricsTotal Citations0Total Downloads145Last 12 Months3Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

We investigate the descriptive succinctness of three fundamental notions for modeling concurrency: nondeterminism and pure parallelism, the two facets of alternation, and bounded cooperative concurrency , whereby a system configuration consists of a bounded number of cooperating states. Our results are couched in the general framework of finite-state automata, but hold for appropriate versions of most concurrent models of computation, such as Petri nets, statecharts or finite-state versions of concurrent programming languages. We exhibit exhaustive sets of upper and lower bounds on the relative succinctness of these features over Σ * and Σ ω , establishing that: For example, we prove exponential upper and lower bounds on the simulation of deterministic concurrent automata by AFAs, and triple-exponential bounds on the simulation of alternating concurrent automata by DFAs.

This is the second in a series of papers on the inherent power of bounded cooperative concurrency, whereby an automaton can be in some bounded number of states that cooperate in accepting the input. In this paper, we consider pushdown automata. We are interested in differences in power of expression and in exponential (or higher) discrepancies in succinctness between variants of pda's that incorporate nondeterminism (E), pure parallelism (A), and bounded cooperative concurrency (C). Technically, the results are proved for cooperating push-down automata with cooperating states, but they hold for appropriate versions of most concurrent models of computation. We exhibit exhaustive sets of upper and lower bounds on the relative succinctness of these features for three classes of languages: deterministic context-free, regular, and finite. For example, we show that C represents exponential savings in succinctness in all cases except when both E and A are present (i.e., except for alternating automata), and that E and A represent unlimited savings in succinctness in all cases.

We consider infinite recursive (i.e., computable) relational data bases. Since the set of computable queries on such data bases is not closed under even simple relational operations, one must either make do with a very modest class of queries or considerably restrict the class of allowed data bases. We define two query languages, one for each of these possibilities, and prove their completeness. The first is the language of quantifier-free first-order logic, which is shown to be complete for the non-restricted case. The second is an appropriately modified version of Chandra and Harel's language QL, which is proved complete for the case of ``highly symmetric" data bases, i.e., ones whose set of automorphisms is of finite index for each tuple-width. We also address the related notion of BP-completeness.

Extensions of propositional dynamic logic (PDL) with nonregular programs are considered. Three classes of nonregular languages are defined, and for each of them it is shown that for any language L in the class, PDL, with L added to the set of regular programs as a new program, is decidable. The first class consists of the languages accepted by pushdown automata that act only on the basis of their input symbol, except when determining whether they reject or continue. The second class (which contains even noncontext-free languages) consists of the languages accepted by deterministic stack machines, but which have a unique new symbol prefixing each word. The third class represents a certain delicate combination of these, and, in particular, it serves to prove the 1983 conjecture that PDL with the addition of the language $\{ {a^i b^i c^i |i \geqslant 0} \}$ is decidable.

The problem of extending the language of statecharts to include overlapping states is considered. The need for such an extension is motivated and the subtlety of the problem is illustrated by exhibiting the shortcomings of naive approaches. The syntax and formal semantics of our extension are then presented, showing in the process that the definitions for conventional statecharts constitute a special case. Our definitions are rather complex, a fact that we feel points to the inherent difficulty of such an extension. We thus prefer to leave open the question of whether or not it should be adopted in practice.

A tight connection is exhibited between infinite paths in recursive trees and Hamiltonian paths in recursive graphs.A corollary is that determining Hamiltonicity in recursive graphs is highly undecidable, viz, Z~complete.This is shown to hold even for highly recursive graphs with outdegree bounded by 3. Hamiltonicit y is thus an example of an interesting graph problem, which is outside the arithmetic hierarchy in the infinite case.The proofi in the paper are nontrivial, yet are elementary in nature.

The problem of deciding the validity of formulas in extensions of propositional dynamic logic (PDL) is considered. The extensions are obtained by adding programs defined by nonregular languages. In the past, a number of very simple languages were shown to render this problem highly undecidable, whereas other very similar-looking languages were shown to retain decidability. Understanding this rather strange phenomenon and generalizing the isolated extensions have remained elusive. The authors provide decision procedures for two wide classes of extensions, thus shedding light on the general problem. The proofs are novel, in that they explicitly consider the machines that accept the languages, in this case special classes of PDAs and stack automata. It is shown that the emptiness problem for stack automata on infinite trees is decidable, a result of independent interest, and the result is combined with the construction of certain tree models for the corresponding formulas.>

For pt.II by T. Hirst and D. Harel see Proc. 15th Coll. Trees in Algebra and programming. Lec. Notes in Comp. Sci., Springer (1990). The difficulty of reasoning about programs is addressed. Specifically, the question of whether the additional succinctness that bounded concurrency provides influences the complexity of reasoning about regular computation sequences on the propositional level is considered. The results concern dynamic, temporal, and process logics, and supply a strongly affirmative answer. In particular, triple-exponential time upper and lower bounds on deciding the validity of propositional dynamic logic with alternating automata enriched with bounded cooperative concurrency, and quadruple-exponential time bounds for deciding validity of branching-time and process logics with such automata are proven. In addition to constituting further evidence for the inherent exponential nature of bounded concurrency, the results appear to provide the first examples of natural decision problems that are elementary and yet have lower bounds that are higher than double-exponential time.>

STATEMATE is a set of tools, with a heavy graphical orientation, intended for the specification, analysis, design, and documentation of large and complex reactive systems. It enables a user to prepare, analyze, and debug diagrammatic, yet precise, descriptions of the system under development from three interrelated points of view, capturing structure, functionality, and behavior. These views are represented by three graphical languages, the most intricate of which is the language of statecharts, used to depict reactive behavior over time. In addition to the use of statecharts, the main novelty of STATEMATE is in the fact that it understands the entire descriptions perfectly, to the point of being able to analyze them for crucial dynamic properties, to carry out rigorous executions and simulations of the described system, and to create running code automatically. These features are invaluable when it comes to the quality and reliability of the final outcome.>

Statecharts have been proposed recently as a visual formalism for the behavioral description of complex systems. They extend classical state diagrams in several ways, while retaining their formality and visual nature. The authors argue that statecharts can be beneficially used as a behavioral hardware description language. They illustrate some of the main features of the approach, including: hierarchical decomposition, multilevel timing specifications and flexible concurrency and synchronization capabilities. The authors also present a VLSI synthesis methodology by which layer area and delay periods can be reduced relative to the conventional finite-state-machine (FSM) synthesis method.>

We present a fast algorithm to produce a graphic matrix representation of sequence homology. The algorithm is based on lexicographical ordering of fragments. It preserves most of the options of a simple naive algorithm with a significant increase in speed. This algorithm was the bais for a program, called DNAMAT, that has been extensively tested during the last three years at the Weizmann Institute of Science and has proven to be very useful. In addition we suggest a way to extend our approach to analyse a series of related DNA or RNA sequences, in order to determine certain common structural features. The analysis is done by 'summing' a set of dot-matrices to produce an overall matrix that displays structural elements common to most of the sequences. We give an example of this procedure by analysing tRNA sequences.

Elementary translations between various kinds of recursive trees are presented. It is shown that trees of either finite or countably infinite branching can be effectively put into one-one correspondence with infinitely branching trees in such a way that the infinite paths of the latter correspond to the “ P -abiding” infinite paths of the former. Here P can be any member of a very wide class of properties of infinite paths. For many properties ??, the converse holds too. Two of the applications involve (a) the formulation of large classes of highly undecidable variants of classical computational problems, and in particular, easily describable domino problems that are III 1 1 -complete, and (b) the existence of a general method for proving termination of nondeterministic or concurrent programs under any reasonable notion of fairness.

A generic translation between various kinds of recursive trees is presented. It is shown that trees of either finite or countably-infinite branching can be effectively put into one-one correspondence with infinitely-branching trees in such a way that the infinite paths of the latter correspond to the “@@@@-abiding” infinite paths of the former. Here @@@@ an be any member of a very wide class of properties of infinite paths. Two of the applications involve the formulation of large classes of π11 variants of classical computational problems, and the existence of a general method for proving termination of nondeterministic or concurrent programs under any reasonable notion of fairness.

With the (necessary) condition that atomic programs in process logic (PL) be binary, we present an algorithm for the translation of a PL formula p into a program $\zeta (p)$ of propositional dynamic logic (PDL) such that a finite path satisfies p if it belongs to $\zeta (p)$. This reduction has two immediate corollaries: 1) validity in this PL can be tested by testing validity of formulas in PDL; 2) all state properties expressible in this PL are expressible in PDL. The translation, however, is of nonelementary time complexity.The significance of the result to the search for natural and powerful logics of programs is discussed.

A logic program consists of a set of Horn clauses, and can be used to express a query on relational data bases. It is shown that logic programs express precisely the queries in YE+ (the set of queries representable by a fixpoint applied to a positive existential query). Queries expressible by logic programs are thus not first order queries in general; nor are all the first order queries expressible as logic programs. A way of adding the negation operator to logic programs is suggested. The resulting set of clausal queries equals FP, the set of first order queries closed under fixpoints (as well as ¬, ∨, 3).

With the (necessary) condition that atomic programs in PL be binary, we present an algorithm for the translation of a PL formula X into a PDL program τ (X) such that a finite path satisfies X iff it belongs to τ (X). This reduction has two immediate corollaries: 1) validity in this PL can be tested by testing validity of formulas in PDL; 2) all finite-path program properties expressible in this PL are expressible in PDL.The translation, however, seems to be of non-elementary time complexity. The significance of the result to the search for natural and powerful logics of programs is discussed.

A logic, Pr(DL), is presented, which enables reasoning about probabilistic programs or, alternatively, reasoning probabilistically about conventional programs. The syntax of Pr(DL) derives from Pratt's first-order dynamic logic and the semantics extends Kozen's semantics of probabilistic programs. An axiom system for Pr(DL) is presented and shown to be complete relative to an extension of first-order analysis. For discrete probabilities it is shown that first-order analysis actually suffices. Examples are presented, both of the expressive power of Pr(DL), and of a proof in the axiom system.

The borderline between decidable and undecidable Propositional Dynamic Logic (PDL) is sought when iterative programs represented by regular expressions are augmented with increasingly more complex recursive programs represented by context-free languages. The results in this paper and its companion [HPS] indicate that this line is extremely close to the original regular PDL. The main result of the present paper is: The validity problem for PDL with additional programs αΔ(β)γΔ for regular α, β and γ, defined as Uiαi; β; γi, is Π11-complete. One of the results of [HPS] shows that the single program AΔ(B) AΔ for atomic A and B is actually sufficient for obtaining Π11- completeness. However, the proofs of this paper use different techniques which seem to be worthwhile in their own right.

This paper is an attempt at laying the foundations for the classification of queries on relational data bases according to their structure and their computational complexity. Using the operations of composition and fixpoints, a Σ-Π hierarchy of height, ω2, called the fixpoint query hierarchy, is defined, and its properties investigated. The hierarchy includes most of the queries considered in the literature including those of Codd and Aho and Ullman. The hierarchy to level ω characterizes the first-order queries, and the levels up to ω are shown to be strict. Sets of queries larger than the fixpoint query hierarchy are obtained by considering the queries computable in polynomial time, queries computable in polynomial space, etc. It is shown that classes of queries defined from such complexity classes behave (with respect to containment) in a manner very similar to the corresponding complexity classes. Also, the set of second-order queries turns out to be the same as the set of queries defined from the polynomialtime hierarchy. Finally, these classes of queries are used to characterize a set of queries defined from language considerations: those expressible in a programming language with only typed (or ranked) relation variables. At the end of the paper is a list of symbols used therein.

We define a process logic PL that subsumes Pratt's process logic, Parikh's SOAPL, Nishimura's process logic, and Pnueli's Temporal Logic in expressiveness. The language of PL is an extension of the language of Propositional Dynamic Logic (PDL). We give a deductive system for PL which includes the Segerberg axioms for PDL and prove that it is complete. We also show that PL is decidable.

A simple tree-like programming/specification language is presented. The central idea is the dividing of conventional programming constructs into the two classes of and and or subgoaling, the subgoal tree itself constituting the program. Programs written in the language can, in general, be both nondeterministic and parallel. The syntax and semantics of the language are defined, a method for verifying programs written in it is described, and the practical significance of programming in the language assessed. Finally, some directions for further research are indicated.

The problem of reasoning about recursive programs is considered. Utilizing a simple analogy between iterative and recursive programs viewed as unfinite unions of finite terms, we carry out an investigation analogous to that carried out recently for iterative programs. The main results are the arithmetical completeness of axiom systems for (1) context-free dynamic logic and (2) its extension for dealing with infinite computations. Having the power of expression of these logics in mind, these results can be seen to supply (as corollaries) complete proof methods for the various kinds of correctness of recursive programs.

The concept of a “reasonable” query in a relational data base is investigated. We provide an abstract characterization of the class of queries which are computable, and define the completeness of a query language as the property of being precisely powerful enough to express the queries in this class. Our main result is the completeness of a simple programming language which can be thought of as consisting of the relational algebra augmented with the power of iteration.

We investigate the principles underlying reasoning about nondeterministic programs, and present a logic to support this kind of reasoning. Our logic, an extension of dynamic logic ([22] and [12]), subsumes most existing first-order logics of nondeterministic programs, including that developed by Dijkstra based on the concept of weakest precondition. A significant feature is the strict separation between the two kinds of nonterminating computations: infinite computations and failures. The logic has a Tarskian truth-value semanics, an essential prerequisite to establishing completeness of axiomatizations of the logic. We give an axiomatization for flowchart (regular) programs that is complete relative to arithmetic in the sense of Cook. Having a satisfactory tool at hand, we turn to the clarification of the concept of the total correctness of nondeterministic programs, providing in passing, a critical evaluation of the widely used "predicate transformer" approach to the definition of programming constructs, initiated by Dijkstra [5]. Our axiom system supplies a complete axiomatization of wp.

Dynamic logic is a generalization of first order logic in which quantifiers of the form “for all χ...” are replaced by phrases of the form “after executing program α...”. This logic subsumes most existing first-order logics of programs that manipulate their environment, including Floyd's and Hoare's logics of partial correctness and Manna and Waldinger's logic of total correctness, yet is more closely related to classical first-order logic than any other proposed logic of programs. We consider two issues: how hard is the validity problem for the formulae of dynamic logic, and how might one axiomatize dynamic logic? We give bounds on the validity problem for some special cases, including a Π02-completeness result for the partial correctness theories of uninterpreted flowchart programs. We also demonstrate the completeness of an axiomatization of dynamic logic relative to arithmetic.

Denoting a version of Hoare's system for proving partial correctness of recursive programs by H, we present an extension D which may be thought of as H υ {@@@@,@@@@,@@@@,@@@@} υ H-1, including the rules of H, four special purpose rules and inverse rules to those of Hoare. D is shown to be a complete system (in Cook's sense) for proving deductions of the form σ1,....σn @@@@ σ over a language, the wff's of which are assertions in some assertion language L and partial correctness specifications of the form p(α)q. All valid formulae of L are taken as axioms of D. It is shown that D is sufficient for proving partial correctness, total correctness and program equivalence as well as other important properties of programs, the proofs of which are impossible in H. The entire presentation is worked out in the framework of nondeterministic programs employing iteration and mutually recursive procedures.