We propose to directly synthesise formal verification formulas for multiple model checkers from naturallanguage requirements. Our approach utilises arrangements of logic-labelled finite-state machines (LLFSMs) to construct executable behaviour models. We can then prepare both the model (as a Kripke structure) and associated verification properties as input for each model checker, generating code in several programming languages as well, ensuring identical execution traces across all generated artefacts. We introduce a grammar-prompted Large Language Model (LLM) approach to obtain the Structured English Grammar (SEG) formula for the requirements, complementing the verification of these executable models without semantic gaps, using precisely the same traces in programming languages as well as model checkers. Our tools translate the full set of patterns of SEG formulas automatically to the specific syntax of five different model checkers, sparing developers from the steep learning curv e of mathematical formalisms for model checking, including the differences in syntax these model checkers require, even for the same temporal logic formalism, such as Linear Temporal Logic (LTL) or Computation Tree Logic (CTL). This work significantly reduces barriers to the adoption of formal methods, by enabling developers to work with familiar finite-state machine notation and natural language requirements while attaining formally verified properties and taking advantage of the particular, individual strengths of multiple model checkers.

Formally verifiable, executable models allow the high-level design, implementation, execution, and validation of reliable systems. But, unbounded complexity, semantic gaps, and combinatorial state explosion have drastically reduced the use of model-driven software engineering for even moderately complex real-time systems. We introduce a new solution that enables high level, executable models of decomposable real-time systems. Our novel approach allows verification in both the time domain and the value domain. We show that through 1) the use of a static, worst-case execution time, and 2) our time-triggered deterministic scheduling of arrangements of logic-labelled finite-state machines (LLFSMs), we can create succinct Kripke structures that are fit for formal verification, including verification of timing properties. We leap further and enable parallel, non-preemptive scheduling of LLFSMs where verification is feasible as the faithful Kripke structure has bounded size. We evaluate our approach through a case study where we fully apply a model-driven approach to a hard time-critical system of parallel sonar sensors.

Abstract RoboCup is one of the major global AI events, gathering hundreds of teams from the world’s best universities to compete in various tasks ranging from soccer to home assistance and rescue. The commonality of these three seemingly dissimilar tasks is that in order to perform well, the robot needs to excel at the all major AI tasks: perception, control, navigation, strategy and planning. In this work, we focus on the first of these by presenting what is—to our knowledge—the first fully neural vision system for the Nao robot soccer. This is a challenging task, mainly due to the limited computational capabilities of the Nao robot. In this paper, we propose two novel neural network architectures for semantic segmentation and object detection that ensure low-cost inference, while improving accuracy by exploiting the properties of the environment. These models use synthetic transfer learning to be able to learn from a low number of hand-labeled images. The experiments show that our models outperform state-of-the-art methods such as Tiny YOLO at a fraction of the cost.

The exceptionally high virulence of COVID-19 and the patients' precondition seem to constitute primary factors in how pro-inflammatory cytokines production evolves during the course of an infection. We present a System Dynamics Model approach for simulating the patient reaction using two key control parameters (i) virulence, which can be moderate or high and (ii) patient precondition, which can be healthy, not so healthy or serious preconditions. In particular, we study the behaviour of Inflammatory (M1) Alveolar Macrophages, IL6 and Active Adaptive Immune system as indicators of the immune system response, together with the COVID viral load over time. The results show that it is possible to build an initial model of the system to explore the behaviour of the key attributes involved in the patient condition, virulence and response. The model suggests aspects that need further study so that it can then assist in choosing the correct immunomodulatory treatment, for instance the regime of application of an Interleukin 6 (IL-6) inhibitor (tocilizumab) that corresponds to the projected immune status of the patients. We introduce machine learning techniques to corroborate aspects of the model and propose that a dynamic model and machine learning techniques could provide a decision support tool to ICU physicians.

We propose a new clustering technique called HeMI++. It uses cleansing and cloning operations that help to produce sensible clusters. HeMI++ learns necessary properties of a good clustering solution for a dataset from a high-quality initial population, without requiring any user input. It then disqualifies the chromosomes that do not satisfy the properties through its cleansing operation. In the cloning operation, HeMI++ replaces the chromosomes by high-quality chromosomes already found in the initial population. We compare HeMI++ with six (6) existing techniques on twenty (20) publicly available datasets using the Tree Index metric. Our experimental results indicate a clear superiority of HeMI++ over existing methods. We also apply HeMI++ on a brain dataset and demonstrate its ability to produce sensible clusters.

There is exciting news in recent developments suggesting the potential to treat some human cancers by stimulating the patients own immune system. However, there is still much to understand; therefore, modelling the battle between those cells that are constituents of the human immune system against tumorous cells can significantly provide insights as mathematical modelling has done regarding the immune system behaviour against virus infections. In this paper we innovate in two directions. First, we move the modelling of immune struggles from the sphere of ordinary-differential equation models to the modelling by multi-agent simulations. We highlight the advantages of the multi-agent simulation, for example the consideration of elaborate spatial proximity interactions. Secondly, we move away from the realm of infectious diseases to the complex modelling of the stimulation of T-cells and their participation in fighting cancerous cell tumours.

We introduce and describe an algorithmic transformation from the formalism of arrangements of logic-labelled finite-state machines (LLFSMs) into NuSMV modules (and its implementation as a model-to-model ATL transformation from an Ecore meta-model to the NuSMV language). Our transformation benefits from using modules and integers of NuSMV to improve the efficiency in the construction and verification of the model. Moreover, we can handle predicates about time. Thus, we enable verification of LLFSMs in the time domain. Our transformation is a considerable improvement in efficiency. Compared with earlier transformation algorithms developed by us, the one presented here produces concise NuSMV files (in an example, 130,295 lines were reduced to 418). We thus show that it is possible to automatically translate arrangements of LLFSMs to concise models that can be efficiently and formally verified.

How can there be Human-In-the-Loop-Learning (HILL) if datasets aimed at building classifiers have ever more dimensions? We make two contributions. First, we examine the few early results on the effectiveness of HILL for building autonomous classifiers and report on our own experiment that validates the merits of HILL. Second, we introduce a HILL system (by using parallel coordinates) for learning of decision tree classifiers (DTCs). DTCs importantly emphasise the relevance of attributes and enable attribute selection, and therefore are appreciated for their transparency. The proposed system addresses a number of the shortcomings of the many HILL systems and allows for easy exploration of datasets. In particular, we incorporate parallel coordinates effectively in our tool for visualisation of high dimensional datasets. We can not only focus the learning on the accuracy of classifiers, but we can enhance performance in other important factors such as system's interpretability and the ability to gain insight into datasets. Finally, we show the advantages of our HILL system in the application area of mobile robotics using the case study of image segmentation in robotic soccer.

The World-Wide-Web is a well-established source of resources for different applications and purposes including the support to learning and teaching tasks. The notion of Learning Object (LO) was specifically designed for sharing digital learning materials over web-applications enabling repositories of LOs. But, the extension of such repositories is rather small compared to the Web, and some of these repositories are domain-dependent. LOs typically provide some educational metadata describing the content. However, the WEB hosts hundreds of thousands of web-pages with educational content but with no educational metadata. Generic search engines provide the best current support to sieve such educational web-pages. But such present systems are not educational focused, so they may not pick instructional features that the users want or need for their educational task. We study a web-based retrieval method for using the Web as a repository of educational resources. Our proposal is a new structured scoring method named Educational Ranking Principle (ERP). ERP analyses the suitability of a web-page for teaching a concept in a specific educational context. Our approach shows a superior accuracy performance than Google, TFIDF and BM25F. The results of our experiment using MAP and P@1 undoubtedly confirm the improvement of ERP when compared to all the baselines (with a p-value less than 0.05). Moreover, ERP is the only method where our results have statistical support for higher accuracy than Google for all the four accuracy measures we use in this study.

Search engines and recommender system take advantage of user queries, characteristics, preferences or perceived needs for filtering results. In contexts such as education, considering the purpose of a resource is also fundamental. A document not suitable for learning, although well related to the query, should never be recommended to a student. However, users are currently obliged to spend additional time and effort for matching the machine-filtered results to their purpose. This paper presents a method for automatically filtering web-pages according to their educational usefulness. Our ground truth is a dataset where items are web-pages classified as relevant for education or not. Then, we present a new feature selection method for lowering the number of attributes of the items. We build a committee of feature selection methods, but do not use it as an ensemble. A comprehensive evaluation of our approach against current practices in feature selection and feature reduction demonstrates that our proposal 1) enables state-of-the-art classifiers to perform a significantly faster, yet very accurate, automatic filtering of educational resources, and 2) such filtering meaningfully considers the usefulness of the resource for educational tasks.

Online social networks (OSNs) are currently a popular platform for social interactions among people. Usually, OSN users upload various contents including personal information on their profiles. The ability to infer users' hidden information or information that has not been even uploaded (i.e. private/sensitive information) by an unauthorised agent is commonly known as attribute inference problem. In this paper, we propose 3LP+, a privacy-preserving technique, to protect users' sensitive information leakage. We apply 3LP+ on a synthetically generated OSN data set and demonstrate the superiority of 3LP+ over an existing privacy-preserving technique.

For the UML, state charts are by far the most used modelling tools, both to communicate behaviour and to produce executable models. We investigate the inherent asymmetry of On-Entry and On-Exit Actions in UML Statecharts. We show first that the apparently simple and symmetric rules for handling the sequencing of On-Entry and On-Exit actions are hard to fully comprehend and apply effectively by software developers. Second, defining a semantics that results in executable models for applications such as reactive-systems and real-time systems is very delicate. Third, formal verification can be hampered because the semantics results in a combinatorial explosion of states. We evaluate the understandability of the semantics by taking out experiments with various tasks comprising sample UML Statechart and logic-labelled finite state machines (LLFSMs). Several experiments with software developers enable us to dissect how issues of understandability of state diagrams relate to nesting or event-driven vs logic-labelled. Since logic-labelled finite state machines achieve model composition through a subsumption architecture (suspend/restart/resume) we propose a specific alternative semantics for logic-labelled finite state machines that is suitable for robotic and embedded systems.

Logic-labeled Finite-State Machines (LLFSMs) are Communicating Extended Finite State Machines that execute concurrently but with a predefined sequential schedule. This capacity has enabled effective formal verification. Moreover, LLFSMs are very powerful tools for Model-Driven Software Engineering of the behaviour of robotic and embedded systems. Although existing schedulers are capable of executing several instances of the same model, the challenge is to provide mechanisms for creating parameterised models akin to function calls. Since recent task planning algorithms can synthesise behaviours as LLFSMs with parameters and recursion, it becomes necessary to have a useful operational tool that produces compiled executables for such behaviours. Moreover, parameterisation allows replication of generic system components, reducing overall design complexity. We produce safe mechanisms to set actual and formal parameters for multiple, concurrent instances of the same behaviour. We achieve the parameterisation of behaviour models analogous to a procedural abstraction and discuss its advantages and disadvantages on formal verification.

We show an architecture that enables runtime verification. Runtime verification focusses on the design of formal languages for the specification of properties that must hold during runtime. In this paper, we take matters one step further and describe a uniform modelling and development paradigm for software systems that can monitor the quality of software systems as they execute, set-up, tear-down and enforce quality behaviour on the fly. Our paradigm for modelling behaviour enables efficient execution, validation, simulation, and runtimeverification. The models are executable and efficient because they are compiled (not interpreted). Moreover, they can be developed using test-driven development, where tests are models derived from requirements. We illustrate the approach with case studies from robotics and embedded systems.

In the Technology Enhanced Learning (TEL) community, the problem of conducting reproducible evaluations of recommender systems is still open, due to the lack of exhaustive benchmarks. The few public datasets available in TEL have limitations, being mostly small and local.

Using the web for communication, purchases, searching information and/or socializing generates data, about ourselves, our connections and our activities, which is collected easily. In online social networks, users volunteer perhaps what is considered more personal information to their selected circles. But each person has personal preferences about what it considers public and what it considers private. The problem is that the information that is public may be used to disclose information that the users expect to remain confidential.

There are many areas where software components must interact witch each other and where middleware provides the appropriate benefits of robustness, decoupling, and modularisation. However, there is a potential performance overhead that, for autonomous robotic and embedded systems, may be critical. Proposals for robotic middleware continue to emerge, but surprisingly, they repeatedly follow the publish-subscriber model. There are several disadvantages to the push paradigm of the publisher-subscriber approach; in particular, its implication of a closer coupling where the subscriber must be active and able to keep up with the pace of events. We propose an alternative pull model, where consumers of messages handle information at their own time. We show that our proposal aligns with fundamental, time-triggered design principles, and produces simple module communication that reduces thread management and can enable rapid prototyping, validation, and formal verification.

Millions of users place data about themselves on on-line social networks and, while probably they have an interest on some of this information to be publicly available, they certainly may consider some of this information shall remain confidential. Simultaneously, the data provides benefits as such data enables personalization which increases the quality of service; and thus, it is regularly analyzed with data mining techniques. Since privacy directly correlates to the control users have regarding the data about themselves, this paper provides a technique by which operators of on-line social networks can improve the service to their users by empowering the users to appraise the privacy risks that some information they provide results in others inferring confidential attributes.

We propose vectors of finite-state machines whose transitions are labeled by formulas of a common-sense logic as the modeling tool for embedded systems software. We have previously shown that this methodology is very efficient in producing succinct and clear models (e.g., in contrast to plain finite-state machines, Petri nets, or Behavior Trees). We show that we can capture requirements precisely and that we can simulate and validate the models. We can, therefore, directly apply Model-Driven Engineering and deploy the models into software for diverse platforms with full tractability of requirements. Moreover, the sequential semantics of our vector of finite-state machines enables model-checking, formally establishing the correctness of the model. Finally, our approach facilitates systematic Failure Modes and Effects Analysis (FMEA) for diverse target platforms. We demonstrate the effectiveness of our methodology with several examples widely discussed in the software engineering literature and compare this with other approaches, showing that we can prove more properties, and that some claims about verification in such approaches have been exaggerated or are incomplete.

Privacy concerns may discourage users who would otherwise join beneficial data mining tasks for intelligence and/or security. We propose an efficient protocol that allows parties to share data in a private way with no restrictions and without loss of accuracy. Our method has the immediate application that horizontally partitioned databases can be brought together and made public without disclosing the source/owner of each record. At another level, we have an additional benefit that we can apply our protocol to privately discover association rules. Our protocol is more efficient than previous methods. The effects of our protocol are less than others: 1) each party can identify only their data, 2) no party is able to learn the links between other parties and their data, 3) no party learns any transactions of the other parties' databases.

The World Wide Web (WWW) and its associated browser-server technologies have become ubiquitous for the home, office and school environment. In the area of education, it has been argued that students can learn new ways of thinking and understanding by working in groups by P. Feltovich et al. (1996). We have developed a tool that allows a group of users to conduct unconstrained collaborative browsing sessions in real-time over the WWW. We have conducted usability studies with volunteer students from South East Queensland, Australia. Our results show that students learnt to use the tool effectively and enjoyed using it.

A-scans from ultrasonic testing of long shafts are complex signals. The discrimination of different types of echoes is of importance for nondestructive testing and equipment maintenance. Research has focused on selecting features of physical significance or exploring classifier like artificial neural networks and support vector machines. This paper confirms the observation that there seems to be uncorrelated errors among the variants explored in the past, and therefore an ensemble of classifiers is to achieve better discrimination accuracy. We explore the diverse possibilities of heterogeneous and homogeneous ensembles, combination techniques, feature extraction methods and classifiers types and determine guidelines for heterogeneous combinations that result in superior performance.

The most common task being performed on the World Wide Web, namely exploring its contents remains an individual rather than a cooperative, shared or partnered activity. We propose that the existing model of collaborative browsing, namely master/slave, is too restrictive. Instead, we introduce group unified histories to provide unconstrained cooperative browsing. Our approach is founded on a persistent shared history object which is replicated for each user and totally configurable. In order for cooperation to succeed users are updated of changes taking place and shown the history of documents within the context of the group. Replication means that consistency needs to be maintained. We show that unconstrained cooperative browsing is a subset of collaborative editing, and using the consistency model of real-time collaborative editors achieves consistency and provides awareness in group unified histories.

The automatic tracking of bees while pollinating macadamia trees is important for the understanding of reproductive biology and fruit yield. We present techniques for tracking these small targets in an uncontrolled illumination environment and where the background is not fixed. Our results indicate we can track, based on color, bees moving in 3D in paths over 3s long (72 frames).

Research has focused significantly in enabling the Web (WWW) for computer supported cooperative work (CSCW). However, surfing, the most common use in the WEB, remains an individual, rather than group activity. Previous attempts to provide collaborative browsing capability constrain some users to the command of a selected user who controls the browsers of others. We adapt the technology of unconstrained distributed collaborative editors to develop unconstrained collaborative Web browsing. However, the effective collaboration is dependent on the awareness of context and group activity. We develop the history mechanisms for our solution to provide 4 types of awareness commonly discussed in the literature of CSCW.

We study several tested cases of the error-correcting graph isomorphism problem. The set Sn of n! permutations on n items is the search space for this optimization problem. We apply MA-sorting. This is a memetic algorithm with domain-independent mutation operators based on classical sorting. Each sorting algorithm works on results to a comparison predicate and defines a path in SI.,. In MA-sorting the mutation operator is a local-search that evaluates permutations suggested by the sorting algorithm. When such evaluation results in an improvement, the mutation is accepted and the comparison operator of the sorting algorithm evaluates to true. In contrast with previous proposals, our MA-sorting instantiated with selection sort finds optimal solutions for this case study.

A sorting algorithm defines a path in the search space of n! permutations based on the information provided by a comparison predicate. Our generic mutation operator for hybridization is a hill-climber and follows the path traced by any sorting algorithm. Our proposal adds exploitation capability to the mutation operator. Mutation requests swaps to construct and test new permutations, while the sorting algorithm supplies suggestions for swapping pairs as comparison to perform. The need to compare pairs of items in sorting is fulfilled by evaluating a guiding function. This novel HGA-sorting hybrid, instantiated with Insertion Sort, dramatically improves previous results for a benchmark of experiments of the Error-Correcting Graph Isomorphism.

This paper reviews approaches for automated pattern spotting and knowledge discovery in spatially referenced data. This is an emerging field which to date has received developmental contributions primarily from researchers in statistics and knowledge discovery in databases (KDD). The field of geographical information systems (GIS) has, however, recognized its importance as a means for providing more exploratory analysis functionality. Tools based upon automated approaches that identify potentially important relationships in spatial data are essential in GIS in order to effectively deal with the increasing amounts of information being gathered. Clustering techniques are proving to be valuable, but there appears to be a general lack of understanding associated with the use and application of various clustering methods in the geographic domain. Further, there is little if any recognition of the relationships between clustering methods. As a result, the development of techniques known to be problematic or inferior has occurred. This paper presents an overview of clustering methods for exploratory spatial data analysis and associated application issues.

Inductive inference techniques that allow symbolic representation of the acquired knowledge facilitate knowledge validation, revision and understanding by human experts. EVOPROL v 1.1 (Evolutionary Propositional Logic) is an inductive, efficient, versatile system for supervised learning of logic rules using a genetic algorithm. EVOPROL contributes to computer assisted knowledge acquisition because it allows discovery of flexible and/or alternative rules from examples. The approach presented in the paper integrates sources of knowledge and establishes collaboration between the genetic searcher and the human expert.