Search

Highlights • And-cross transitions are a useful abstraction that can make some constructs easier to specify for the modeler. • They can be transformed to and from alternative modeling solutions that require a greater number of transitions. • With fewer transitions, the time taken and memory required to certify a model to be deterministic using formal methods can be much reduced compared to other approaches. This is related to the time and memory required to compute the set of pairs of potentially conflicting transitions. Abstract In this paper, we present an approach to formally encode state machines expressed in Umple for symbolic verification. We illustrate this with a real-world modeling example that encodes and analyzes and-cross transitions. This paper discusses a formal description of our approach to represent state machine systems under analysis (SSUAs); a systematic approach to certifying that SSUAs are deterministic; and an evaluation of performance (memory usage and execution time) on the case study. Method We describe a formalization of state machines in Umple that enables their translation to model checking tools and also to code that is consistent with this. We present three alternative modeling solutions for a sample problem and a solution based on the use of and-cross transitions. State machine models corresponding to these solutions are represented in Umple, a model-oriented programming language. These are automatically transformed to SMV, the input language of the nuXmv (or NuSMV) model checker. By cleanly separating concerns, we systematically integrate components of hierarchical state systems as opposed to the traditional flattening approach, yet manage the complexity introduced by concurrency and and-crossing. We then compose and verify a set of requirements (e.g., correctness, safety, liveliness, etc.) on the resulting systems of all the modeling approaches to empirically compare the different modeling alternatives with the use of and-cross transitions. Results We can encode and formally analyse complex state machines with and-cross transition(s). We observed a large reduction in the number of required transitions for encoding the SSUA, as opposed to the alternative approaches. We asserted that solutions derived from the approaches are identical behavior-wise even though each approach models the SSUA differently. Each of the approaches yielded the same result for potentially conflicting pairs which is a false positive (i.e., the SSUAs are deterministic). We observe that each approach maintains the same global state-space irrespective of the variations in their number of transitions. Furthermore, we observe that it is untrue that a more abstract method applied to an SSUA outperforms its less abstract counterpart whenever parameters (such as execution time, memory usage and the number of Binary Decision Diagrams - BDDs) are the factors under consideration. Contributions A systematic approach to encode state machines with and-cross transitions (including unusual transitions). An enhanced but fully automated approach to discovering nondeterminism in state machines even in the presence of unbounded domains and multiple and-cross transitions within the same enclosing orthogonal state. An empirical study of the impact of abstraction on some performance parameters. We also present an extended formalization of Umple state machines. [ABSTRACT FROM AUTHOR]

• We establish the first mathematical model for portraying inner behaviors and computational procedures of mimic computing. • We propose a novel type of automata called mimic automata, i.e., the new model mentioned above. • The formal semantic and expressive ability of the new automata is obtained. • In an application scene, this new model is employed to address a problem on systematic structures of mimic computers. In this paper, we aim to establish a mathematical model for mimic computing. To this end, we present a novel automaton called a mimic automaton. First, a one-dimensional cellular automaton is used for expressing some dynamic changes in the structure of a computing unit, a sequential automaton is employed to describe some state transitions, a hierarchical automaton is employed to express the different granularities of some computing units, and a probabilistic automaton is used to depict some random changes of a computing unit. Second, a mimic automaton is obtained by combining the various types of automata mentioned above in a certain logical relationship. Compared with the existing models of mimic computing, the new model portrays the operational semantics for a mimic computing system, and it can directly describe the behaviors of a system. Furthermore, the new model possesses a stronger generality. [ABSTRACT FROM AUTHOR]

This paper presents spiking neural P systems with weighted synapses, a class of distributed parallel neural-like computing models, abstracted from the way in which the complex system of neurons processes information and communicates to ensure a proper functioning of the brain. Neurons communicate with each other through synapses endowed with an integer weight denoting the number of synapses for each pair of connected neurons. We translate the spiking neural P systems with weighted synapses into a class of timed safety automata, proving that such a translation is formally correct. This relationship allows the verification of several kinds of properties, both qualitative and quantitative, using tools and techniques developed for timed automata. [ABSTRACT FROM AUTHOR]

In this paper, we develop a framework for an efficient under-approximation of the dynamics of Asynchronous Automata Networks (AANs). An AAN is an Automata Network with synchronised transitions between automata, where each transition changes the local state of exactly one automaton (but any number of synchronising local states are allowed). The work we propose here is based on static analysis by abstract interpretation, which allows to prove that reaching a state with a given property is possible, without the same computational cost of usual model checkers: the complexity is polynomial with the total number of local states and exponential with the number of local states within a single automaton. Furthermore, we address AANs with classes of priorities, and give an encoding into AANs without priorities, thus extending the application range of our under-approximation. Finally, we illustrate our method for the model checking of large-scale biological networks. [ABSTRACT FROM AUTHOR]

De Alfaro and Henzinger introduced interface automata to model and study behavioural types. These come with alternating simulation as refinement and with a specific parallel composition: if one component receives an unexpected input, this is regarded as an error and the resp. error states are removed with a special pruning operation. In this paper, we return to the foundations of interface automata and study how refinement and parallel composition should be defined best. We take as basic requirement that an implementation must be error-free, if the specification is. For three variants of error-free, we consider the coarsest precongruence for parallel composition respecting the basic requirement. We find that pruning proves to be relevant in all cases and point out an important subtlety for systems that are not input-deterministic. [ABSTRACT FROM AUTHOR]

Abstract: Context-Free Grammars (CFGs) and Parsing Expression Grammars (PEGs) have several similarities and a few differences in both their syntax and semantics, but they are usually presented through formalisms that hinder a proper comparison. In this paper we present a new formalism for CFGs that highlights the similarities and differences between them. The new formalism borrows from PEGs the use of parsing expressions and the recognition-based semantics. We show how one way of removing non-determinism from this formalism yields a formalism with the semantics of PEGs. We also prove, based on these new formalisms, how grammars define the same language whether interpreted as CFGs or as PEGs, and also show how strong- , right-linear, and LL-regular grammars have simple language-preserving translations from CFGs to PEGs. Once these classes of CFGs can be automatically translated to equivalent PEGs, we can reuse classic top-down grammars in PEG-based tools. [Copyright &y& Elsevier]

Abstract: The study of the behaviour of non-deterministic automata has traditionally focused on the languages which can be associated to the different states. Under this interpretation, the different branches that can be taken at every step are ignored. However, we can also take into account the different decisions which can be made at every state, that is, the branches that can be taken, and these decisions might change the possible future behaviour. In this case, the behaviour of the automata can be described with the help of the concept of bisimilarity. This is the kind of description that is usually obtained when the automata are regarded as labelled transition systems or coalgebras. Contrarily to what happens with deterministic automata, it is not possible to describe the behaviour up to bisimilarity of states of a non-deterministic automaton by considering just the languages associated to them. In this paper we present a description of a final object for the category of non-deterministic automata, regarded as labelled transition systems, with the help of some structures defined in terms of languages. As a consequence, we obtain a characterisation of bisimilarity of states of automata in terms of languages and a method to minimise non-deterministic automata with respect to bisimilarity of states. This confirms that languages can be considered as the natural objects to describe the behaviour of automata. [Copyright &y& Elsevier]

Abstract: Finite State Machines (FSMs) are widely used for verification and testing of many reactive systems and many methods are proposed for generating tests from FSMs with the guaranteed fault coverage. However, some systems can only be properly described when time constraints are considered, advocating the adoption of models with the notion of time. In this paper, a method for deriving conformance tests with the guaranteed fault coverage from a Timed FSM (TFSM) with a single clock is presented. Test derivation is based on a given fault domain that allows the derivation of test suites with reasonable length. More precisely, the fault domain includes every possible faulty TFSM implementation with the known largest time constraints boundaries and minimal duration of time guards. Given a deterministic possibly partial TFSM specification, a complete test suite that guarantees the detection of all faulty implementations with respect to the above fault domain is derived. Experiments with randomly generated timed FSMs are conducted to determine length of obtained test suites and assess the impact of varying the TFSM specification parameters on length of obtained test suites. Further, experiments with both untimed and timed machines are conducted and these experiments show that similar patterns for timed and untimed machines are obtained with respect to varying the number of states, inputs, and outputs of machines. [Copyright &y& Elsevier]

Abstract: Many electoral control and manipulation problems—which we will refer to in general as “manipulative actions” problems—are NP-hard in the general case. It has recently been noted that many of these problems fall into polynomial time if the electorate is single-peaked, i.e., is polarized along some axis/issue. However, real-world electorates are not truly single-peaked. There are usually some mavericks, and so real-world electorates tend merely to be nearly single-peaked. This paper studies the complexity of manipulative-action algorithms for elections over nearly single-peaked electorates. We do this for many notions of nearness and for a broad range of election systems. We provide instances where even one maverick jumps the manipulative-action complexity up to NP-hardness, but we also provide many instances where some number of mavericks can be tolerated without increasing the manipulative-action complexity. [Copyright &y& Elsevier]

Abstract: Recently, there has been a significant increase in studies employing auditory models in speech recognition systems. In this paper, we propose a new evolutionary tuned feature extraction method by spectro-temporal analysis. In our proposed model, there is a special subspace for each phoneme with a specific best scale in the spectral filter and a specific best rate in the temporal filter. These two parameters were obtained by genetic cellular automata evolutionary algorithm. The extracted features from the specific subspace are classified by a binary one-versus-rest support vector machine. Finally, a multiclass classifier for all phonemes is employed by combining these sub-models. The proposed method improved the discrimination of phonemes significantly especially in highly confusable phonemes. To show the efficiency of the proposed feature sets, it was empirically compared with two baseline models. The achieved relative improvements are about 10% in classification rate for voiced plosives, unvoiced plosives and nasals; and about 7.38% for front vowels relative to the state of the art baseline model. [Copyright &y& Elsevier]

Abstract: Process models discovered from a process log using process mining tend to be complex and have problems balancing between overfitting and underfitting. An overfitting model allows for too little behavior as it just permits the traces in the log and no other trace. An underfitting model allows for too much behavior as it permits traces that are significantly different from the behavior seen in the log. This paper presents a post-processing approach to simplify discovered process models while controlling the balance between overfitting and underfitting. The discovered process model, expressed in terms of a Petri net, is unfolded into a branching process using the event log. Subsequently, the resulting branching process is folded into a simpler process model capturing the desired behavior. [Copyright &y& Elsevier]

Abstract: Refinement is a relation on system models: a concrete model is a refinement of a more abstract model if it has fewer behaviors. When properties of the abstract model are guaranteed to be preserved in the concrete model, refinement supports a top-down development process. This paper considers preservation of a range of information flow security properties in synchronous systems with schedulers, when these schedulers are refined. Notions of refinement are defined for both an abstract notion of scheduler as well as for their concrete representation as automata. The security properties that are preserved by refinement over schedulers are then characterized. The results are applied to characterize a number of scheduler independent security properties, which state that a system is secure with respect to all schedulers. [Copyright &y& Elsevier]

Abstract: Recent years have seen a great deal of work that exploits collaborative, semi-structured content for Artificial Intelligence (AI) and Natural Language Processing (NLP). This special issue of the Artificial Intelligence Journal presents a variety of state-of-the-art contributions, each of which illustrates the substantial impact that work on leveraging semi-structured content is having on AI and NLP as it continuously fosters new directions of cutting-edge research. We contextualize the papers collected in this special issue by providing a detailed overview of previous work on collaborative, semi-structured resources. The survey is made up of two main logical parts: in the first part, we present the main characteristics of collaborative resources that make them attractive for AI and NLP research; in the second part, we present an overview of how these features have been exploited to tackle a variety of long-standing issues in the two fields, in particular the acquisition of large amounts of machine-readable knowledge, and its application to a wide range of tasks. The overall picture shows that not only are semi-structured resources enabling a renaissance of knowledge-rich AI techniques, but also that significant advances in high-end applications that require deep understanding capabilities can be achieved by synergistically exploiting large amounts of machine-readable structured knowledge in combination with sound statistical AI and NLP techniques. [Copyright &y& Elsevier]

Abstract: ASM refinements are verified using generalized forward simulations which allow us to refine m abstract operations to n concrete operations with arbitrary m and n. One main difference from data refinement is that ASM refinement considers infinite runs and termination. Since backward simulation does not preserve termination in general, the standard technique of adding history information to the concrete level is not applicable to get a completeness proof. The power set construction also adds infinite runs and is therefore not applicable either. This paper shows that a completeness proof is nevertheless possible by adding infinite prophecy information, effectively moving nondeterminism to the initial state. Adding such prophecy information can be done not only on the semantic level, but also by a simple syntactic transformation that removes the choose construct of ASMs. The completeness proof is also translated to a completeness proof for IO automata. Finally, the proof is extended to deal with supplementary predicates, that specify fairness and liveness assumptions, by transferring a related result of Wim Hesselink for refinements that use the Abadi–Lamport setting. [Copyright &y& Elsevier]

Abstract: Looking for small universal computing devices is a natural and well investigated topic in computer science. Recently, this topic was also investigated in the framework of spiking neural P systems. One of the small universality results is that a small weakly universal extended spiking neural P system with 12 neurons was constructed. In this paper, a new way is introduced for simulating register machines by spiking neural P systems, where only one neuron is used for all instructions of the register machine; in this way, we can use less neurons to construct universal spiking neural P system. Specifically, we give a smaller weakly universal spiking neural P system that uses extended rules and has only 9 neurons. [Copyright &y& Elsevier]

Abstract: Stream X-machines are a state based formalism that has associated with it a particular development process in which a system is built from trusted components. Testing thus essentially checks that these components have been combined in a correct manner and that the orders in which they can occur are consistent with the specification. Importantly, there are test generation methods that return a checking experiment: a test that is guaranteed to determine correctness as long as the implementation under test (IUT) is functionally equivalent to an unknown element of a given fault domain . Previous work has show how three methods for generating checking experiments from a finite state machine (FSM) can be adapted to testing from a stream X-machine. However, there are many other methods for generating checking experiments from an FSM and these have a variety of benefits that correspond to different testing scenarios. This paper shows how any method for generating a checking experiment from an FSM can be adapted to generate a checking experiment for testing an implementation against a stream X-machine. This is the case whether we are testing to check that the IUT is functionally equivalent to a specification or we are testing to check that every trace (input/output sequence) of the IUT is also a trace of a nondeterministic specification. Interestingly, this holds even if the fault domain used is not that traditionally associated with testing from a stream X-machine. The results also apply for both deterministic and nondeterministic implementations. [Copyright &y& Elsevier]

Abstract: This paper continues the investigation of population P systems model [F. Bernardini, M. Gheorghe, Population P systems, Journal of Universal Computer Science 10 (5) (2004) 509–539] by considering bacterium quorum sensing (QS) phenomena as the basis of the new approach. A new computational model called QS P system is introduced. It is proved that QS P systems are able to simulate counter machines, and hence they are equivalent in power to Turing machines. An example of a QS P system modelling the behaviour of Vibrio fischeri bacteria colonies is also presented and the emergence of the QS mechanism is illustrated. [Copyright &y& Elsevier]