Istituto di Scienza e Tecnologie
dell’Informazione “A. Faedo”

Speakers:

Alessio Ferrari

Referent:

Andrea Esuli

We present a novel approach for pragmatic ambiguity detection in natural language (NL) requirements specifications defined for a specific application domain. Starting from a requirements specification, we use a Web-search engine to retrieve a set of documents focused on the same domain of the specification. From these domain-related documents, we extract different knowledge graphs, which are employed to analyse each requirement sentence looking for potential ambiguities. To this end, an algorithm has been developed that takes the concepts expressed in the sentence and searches for corresponding "concept paths" within each graph. The paths resulting from the traversal of each graph are compared and, if their overall similarity score is lower than a given threshold, the requirements specification sentence is considered ambiguous from the pragmatic point of view. A proof of concept is given throughout the presentation to illustrate the soundness of the proposed strategy.

NOTE: This seminar is the fourth one of the series of six seminars presented by the winners of the prize "Young researchers ISTI 2013". Alessio Ferrari placed first in the Young researcher category.

Speakers:

Laura Nenzi (IMT Lucca)

Referent:

Mieke Massink

We present a new approach for the design of a synthetic biological circuit whose behavior is specified in terms of signal temporal logic (STL) formulae. We first show how to characterize with STL formulae the input/output behavior of biological modules miming the classical logical gates (AND, NOT, OR). Hence, we provide the regions of the parameter space for which these specifications are satisfied. Given a STL specification of the target circuit to be designed and the networks of its constituent components, we propose a methodology to constrain the behavior of each module, then identifying the subset of the parameter space in which those constraints are satisfied, providing also a measure of the robustness for the target circuit design. This approach, which leverages recent results on the quantitative semantics of Signal Temporal Logic, is illustrated by synthesizing a biological implementation of an half-adder.

Speakers:

Roberta Lanziani (IMT Lucca)

Referent:

Mieke Massink

In this talk we investigate the use of Central Limit Approximation of Continuous Time Markov Chains to verify collective properties of large population models, describing the interaction of many similar individual agents. More precisely, we specify properties in terms of individual agents by means of deterministic timed automata with a single global clock (which cannot be reset), and then use the Central Limit Approximation to estimate the probability that a given fraction of agents satisfies the local specification.