-
NLPGuard: A Framework for Mitigating the Use of Protected Attributes by NLP Classifiers
Authors:
Salvatore Greco,
Ke Zhou,
Licia Capra,
Tania Cerquitelli,
Daniele Quercia
Abstract:
AI regulations are expected to prohibit machine learning models from using sensitive attributes during training. However, the latest Natural Language Processing (NLP) classifiers, which rely on deep learning, operate as black-box systems, complicating the detection and remediation of such misuse. Traditional bias mitigation methods in NLP aim for comparable performance across different groups base…
▽ More
AI regulations are expected to prohibit machine learning models from using sensitive attributes during training. However, the latest Natural Language Processing (NLP) classifiers, which rely on deep learning, operate as black-box systems, complicating the detection and remediation of such misuse. Traditional bias mitigation methods in NLP aim for comparable performance across different groups based on attributes like gender or race but fail to address the underlying issue of reliance on protected attributes. To partly fix that, we introduce NLPGuard, a framework for mitigating the reliance on protected attributes in NLP classifiers. NLPGuard takes an unlabeled dataset, an existing NLP classifier, and its training data as input, producing a modified training dataset that significantly reduces dependence on protected attributes without compromising accuracy. NLPGuard is applied to three classification tasks: identifying toxic language, sentiment analysis, and occupation classification. Our evaluation shows that current NLP classifiers heavily depend on protected attributes, with up to $23\%$ of the most predictive words associated with these attributes. However, NLPGuard effectively reduces this reliance by up to $79\%$, while slightly improving accuracy.
△ Less
Submitted 1 July, 2024;
originally announced July 2024.
-
The role of the Big Geographic Sort in the circulation of misinformation among U.S. Reddit users
Authors:
Lia Bozarth,
Daniele Quercia,
Licia Capra,
Sanja Scepanovic
Abstract:
Past research has attributed the online circulation of misinformation to two main factors - individual characteristics (e.g., a person's information literacy) and social media effects (e.g., algorithm-mediated information diffusion) - and has overlooked a third one: the critical mass created by the offline self-segregation of Americans into like-minded geographical regions such as states (a phenom…
▽ More
Past research has attributed the online circulation of misinformation to two main factors - individual characteristics (e.g., a person's information literacy) and social media effects (e.g., algorithm-mediated information diffusion) - and has overlooked a third one: the critical mass created by the offline self-segregation of Americans into like-minded geographical regions such as states (a phenomenon called "The Big Sort"). We hypothesized that this latter factor matters for the online spreading of misinformation not least because online interactions, despite having the potential of being global, end up being localized: interaction probability is known to rapidly decay with distance. Upon analysis of more than 8M Reddit comments containing news links spanning four years, from January 2016 to December 2019, we found that Reddit did not work as an "hype machine" for misinformation (as opposed to what previous work reported for other platforms, circulation was not mainly caused by platform-facilitated network effects) but worked as a supply-and-demand system: misinformation news items scaled linearly with the number of users in each state (with a scaling exponent beta=1, and a goodness of fit R2 = 0.95). Furthermore, deviations from such a universal pattern were best explained by state-level personality and cultural factors (R2 = {0.12, 0.39}), rather than socioeconomic conditions (R2 = {0.15, 0.29}) or, as one would expect, political characteristics (R2 ={0.06, 0.21}). Higher-than-expected circulation of any type of news (including reputable news) was found in states characterised by residents who tend to be less diligent in terms of their personality (low in conscientiousness) and by loose cultures understating the importance of adherence to norms (low in cultural tightness).
△ Less
Submitted 20 May, 2022;
originally announced May 2022.
-
Insider Stories: Analyzing Internal Sustainability Efforts of Major US Companies from Online Reviews
Authors:
Indira Sen,
Daniele Quercia,
Licia Capra,
Matteo Montecchi,
Sanja Šćepanović
Abstract:
It is hard to establish whether a company supports internal sustainability efforts (ISEs) like gender equality, diversity, and general staff welfare, not least because of lack of methodologies operationalizing these internal sustainability practices, and of data honestly documenting such efforts. We developed and validated a six-dimension framework reflecting Internal Sustainability Efforts (ISEs)…
▽ More
It is hard to establish whether a company supports internal sustainability efforts (ISEs) like gender equality, diversity, and general staff welfare, not least because of lack of methodologies operationalizing these internal sustainability practices, and of data honestly documenting such efforts. We developed and validated a six-dimension framework reflecting Internal Sustainability Efforts (ISEs), gathered more than 350K employee reviews of 104 major companies across the whole US for the (2008-2020) years, and developed a deep-learning framework scoring these reviews in terms of the six ISEs. Commitment to ISEs manifested itself at micro-level -- companies scoring high in ISEs enjoyed high stock growth. This new conceptualization of ISEs offers both theoretical implications for the literature in corporate sustainability, and practical implications for companies and policymakers. To further explore these implications, researchers need to add potentially missing ISEs, to do so for more companies, and establish the causal relationship between company success and ISEs.
△ Less
Submitted 13 April, 2023; v1 submitted 2 May, 2022;
originally announced May 2022.
-
A Maude Implementation of Rewritable Petri Nets: a Feasible Model for Dynamically Reconfigurable Systems
Authors:
Lorenzo Capra
Abstract:
Petri Nets (PN) are a central, theoretically sound model for concurrent or distributed systems but, at least in their classical definition, not expressive enough to represent dynamic reconfiguration capabilities. On the other side, Rewriting Logic has proved to be a natural semantic framework for several formal models of concurrent/distributed systems. We propose a compact, efficient Maude forma…
▽ More
Petri Nets (PN) are a central, theoretically sound model for concurrent or distributed systems but, at least in their classical definition, not expressive enough to represent dynamic reconfiguration capabilities. On the other side, Rewriting Logic has proved to be a natural semantic framework for several formal models of concurrent/distributed systems. We propose a compact, efficient Maude formalization of dynamically reconfigurable PT nets (with inhibitor arcs), using as a running example the specification of a simple, fault-tolerant manufacturing system. We discuss the advantages of such a combined approach, as well as some concerns that it raises.
△ Less
Submitted 15 November, 2021;
originally announced November 2021.
-
Multiple Sclerosis disease: a computational approach for investigating its drug interactions
Authors:
Simone Pernice,
Marco Beccuti,
Greta Romano,
Marzio Pennisi,
Alessandro Maglione,
Santina Cutrupi,
Francesco Pappalardo,
Lorenzo Capra,
Giuliana Franceschinis,
Massimiliano De Pierro,
Gianfranco Balbo,
Francesca Cordero,
Raffaele Calogero
Abstract:
Multiple Sclerosis (MS) is a chronic and potentially highly disabling disease that can cause permanent damage and deterioration of the central nervous system. In Europe it is the leading cause of non-traumatic disabilities in young adults, since more than 700,000 EU people suffer from MS. Although recent studies on MS pathophysiology have been provided, MS remains a challenging disease. In this co…
▽ More
Multiple Sclerosis (MS) is a chronic and potentially highly disabling disease that can cause permanent damage and deterioration of the central nervous system. In Europe it is the leading cause of non-traumatic disabilities in young adults, since more than 700,000 EU people suffer from MS. Although recent studies on MS pathophysiology have been provided, MS remains a challenging disease. In this context, thanks to recent advances in software and hardware technologies, computational models and computer simulations are becoming appealing research tools to support scientists in the study of such disease. Thus, motivated by this consideration we propose in this paper a new model to study the evolution of MS in silico, and the effects of the administration of Daclizumab drug, taking into account also spatiality and temporality of the involved phenomena. Moreover, we show how the intrinsic symmetries of the system can be exploited to drastically reduce the complexity of its analysis.
△ Less
Submitted 1 June, 2020;
originally announced June 2020.
-
Social Interactions or Business Transactions? What customer reviews disclose about Airbnb marketplace
Authors:
Giovanni Quattrone,
Antonino Nocera,
Licia Capra,
Daniele Quercia
Abstract:
Airbnb is one of the most successful examples of sharing economy marketplaces. With rapid and global market penetration, understanding its attractiveness and evolving growth opportunities is key to plan business decision making. There is an ongoing debate, for example, about whether Airbnb is a hospitality service that fosters social exchanges between hosts and guests, as the sharing economy manif…
▽ More
Airbnb is one of the most successful examples of sharing economy marketplaces. With rapid and global market penetration, understanding its attractiveness and evolving growth opportunities is key to plan business decision making. There is an ongoing debate, for example, about whether Airbnb is a hospitality service that fosters social exchanges between hosts and guests, as the sharing economy manifesto originally stated, or whether it is (or is evolving into being) a purely business transaction platform, the way hotels have traditionally operated. To answer these questions, we propose a novel market analysis approach that exploits customers' reviews. Key to the approach is a method that combines thematic analysis and machine learning to inductively develop a custom dictionary for guests' reviews. Based on this dictionary, we then use quantitative linguistic analysis on a corpus of 3.2 million reviews collected in 6 different cities, and illustrate how to answer a variety of market research questions, at fine levels of temporal, thematic, user and spatial granularity, such as (i) how the business vs social dichotomy is evolving over the years, (ii) what exact words within such top-level categories are evolving, (iii) whether such trends vary across different user segments and (iv) in different neighbourhoods.
△ Less
Submitted 24 April, 2020;
originally announced April 2020.
-
An Operational Semantics of Graph Transformation Systems Using Symmetric Nets
Authors:
Lorenzo Capra
Abstract:
Graph transformation systems (GTS) have been successfully proposed as a general, theoretically sound model for concurrency. Petri nets (PN), on the other side, are a central and intuitive formalism for concurrent or distributed systems, well supported by a number of analysis techniques/tools. Some PN classes have been shown to be instances of GTS. In this paper, we change perspective presenting an…
▽ More
Graph transformation systems (GTS) have been successfully proposed as a general, theoretically sound model for concurrency. Petri nets (PN), on the other side, are a central and intuitive formalism for concurrent or distributed systems, well supported by a number of analysis techniques/tools. Some PN classes have been shown to be instances of GTS. In this paper, we change perspective presenting an operational semantics of GTS in terms of Symmetric Nets, a well-known class of Coloured Petri nets featuring a structured syntax that outlines model symmetries. Some practical exploitations of the proposed operational semantics are discussed. In particular, a recently developed structural calculus for SN is used to validate graph rewriting rules in a symbolic way.
△ Less
Submitted 4 September, 2019;
originally announced September 2019.
-
Offline Biases in Online Platforms: a Study of Diversity and Homophily in Airbnb
Authors:
Victoria Koh,
Weihua Li,
Giacomo Livan,
Licia Capra
Abstract:
How diverse are sharing economy platforms? Are they fair marketplaces, where all participants operate on a level playing field, or are they large-scale online aggregators of offline human biases? Often portrayed as easy-to-access digital spaces whose participants receive equal opportunities, such platforms have recently come under fire due to reports of discriminatory behaviours among their users,…
▽ More
How diverse are sharing economy platforms? Are they fair marketplaces, where all participants operate on a level playing field, or are they large-scale online aggregators of offline human biases? Often portrayed as easy-to-access digital spaces whose participants receive equal opportunities, such platforms have recently come under fire due to reports of discriminatory behaviours among their users, and have been associated with gentrification phenomena that exacerbate preexisting inequalities along racial lines. In this paper, we focus on the Airbnb sharing economy platform, and analyse the diversity of its user base across five large cities. We find it to be predominantly young, female, and white. Notably, we find this to be true even in cities with a diverse racial composition. We then introduce a method based on the statistical analysis of networks to quantify behaviours of homophily, heterophily and avoidance between Airbnb hosts and guests. Depending on cities and property types, we do find signals of such behaviours relating both to race and gender. We use these findings to provide platform design recommendations, aimed at exposing and possibly reducing the biases we detect, in support of a more inclusive growth of sharing economy platforms.
△ Less
Submitted 30 March, 2019; v1 submitted 15 November, 2018;
originally announced November 2018.
-
Cloud4IoT: a heterogeneous, distributed and autonomic cloud platform for the IoT
Authors:
Daniele Pizzolli,
Giuseppe Cossu,
Daniele Santoro,
Luca Capra,
Corentin Dupont,
Dukas Charalampos,
Francesco De Pellegrini,
Fabio Antonelli,
Silvio Cretti
Abstract:
We introduce Cloud4IoT, a platform offering automatic deployment, orchestration and dynamic configuration of IoT support software components and data-intensive applications for data processing and analytics, thus enabling plug-and-play integration of new sensor objects and dynamic workload scalability. Cloud4IoT enables the concept of Infrastructure as Code in the IoT context: it empowers IoT oper…
▽ More
We introduce Cloud4IoT, a platform offering automatic deployment, orchestration and dynamic configuration of IoT support software components and data-intensive applications for data processing and analytics, thus enabling plug-and-play integration of new sensor objects and dynamic workload scalability. Cloud4IoT enables the concept of Infrastructure as Code in the IoT context: it empowers IoT operations with the flexibility and elasticity of Cloud services. Furthermore it shifts traditionally centralized Cloud architectures towards a more distributed and decentralized computation paradigm, as required by IoT technologies, bridging the gap between Cloud Computing and IoT ecosystems. Thus, Cloud4IoT is playing a role similar to the one covered by solutions like Fog Computing, Cloudlets or Mobile Edge Cloud. The hierarchical architecture of Cloud4IoThosts a central Cloud platform and multiple remote edge Cloud modules supporting dedicated devices, namely the IoT Gateways, through which new sensor objects are made accessible to the platform. Overall, the platform is designed in order to support systems where IoT-based and data intensive applications may pose specific requirements for low latency, restricted available bandwidth, or data locality. Cloud4IoT is built on several Open Source technologies for containerisation and implementations of standards, protocols and services for the IoT. We present the implementation of the platform and demonstrate it in two different use cases.
△ Less
Submitted 3 October, 2018;
originally announced October 2018.
-
Community Question Answering Platforms vs. Twitter for Predicting Characteristics of Urban Neighbourhoods
Authors:
Marzieh Saeidi,
Alessandro Venerandi,
Licia Capra,
Sebastian Riedel
Abstract:
In this paper, we investigate whether text from a Community Question Answering (QA) platform can be used to predict and describe real-world attributes. We experiment with predicting a wide range of 62 demographic attributes for neighbourhoods of London. We use the text from QA platform of Yahoo! Answers and compare our results to the ones obtained from Twitter microblogs. Outcomes show that the co…
▽ More
In this paper, we investigate whether text from a Community Question Answering (QA) platform can be used to predict and describe real-world attributes. We experiment with predicting a wide range of 62 demographic attributes for neighbourhoods of London. We use the text from QA platform of Yahoo! Answers and compare our results to the ones obtained from Twitter microblogs. Outcomes show that the correlation between the predicted demographic attributes using text from Yahoo! Answers discussions and the observed demographic attributes can reach an average Pearson correlation coefficient of \r{ho} = 0.54, slightly higher than the predictions obtained using Twitter data. Our qualitative analysis indicates that there is semantic relatedness between the highest correlated terms extracted from both datasets and their relative demographic attributes. Furthermore, the correlations highlight the different natures of the information contained in Yahoo! Answers and Twitter. While the former seems to offer a more encyclopedic content, the latter provides information related to the current sociocultural aspects or phenomena.
△ Less
Submitted 17 January, 2017;
originally announced January 2017.
-
Who Benefits from the "Sharing" Economy of Airbnb?
Authors:
Giovanni Quattrone,
Davide Proserpio,
Daniele Quercia,
Licia Capra,
Mirco Musolesi
Abstract:
Sharing economy platforms have become extremely popular in the last few years, and they have changed the way in which we commute, travel, and borrow among many other activities. Despite their popularity among consumers, such companies are poorly regulated. For example, Airbnb, one of the most successful examples of sharing economy platform, is often criticized by regulators and policy makers. Whil…
▽ More
Sharing economy platforms have become extremely popular in the last few years, and they have changed the way in which we commute, travel, and borrow among many other activities. Despite their popularity among consumers, such companies are poorly regulated. For example, Airbnb, one of the most successful examples of sharing economy platform, is often criticized by regulators and policy makers. While, in theory, municipalities should regulate the emergence of Airbnb through evidence-based policy making, in practice, they engage in a false dichotomy: some municipalities allow the business without imposing any regulation, while others ban it altogether. That is because there is no evidence upon which to draft policies. Here we propose to gather evidence from the Web. After crawling Airbnb data for the entire city of London, we find out where and when Airbnb listings are offered and, by matching such listing information with census and hotel data, we determine the socio-economic conditions of the areas that actually benefit from the hospitality platform. The reality is more nuanced than one would expect, and it has changed over the years. Airbnb demand and offering have changed over time, and traditional regulations have not been able to respond to those changes. That is why, finally, we rely on our data analysis to envision regulations that are responsive to real-time demands, contributing to the emerging idea of "algorithmic regulation".
△ Less
Submitted 6 February, 2016;
originally announced February 2016.
-
Measuring Urban Deprivation from User Generated Content
Authors:
Alessandro Venerandi,
Giovanni Quattrone,
Licia Capra,
Daniele Quercia,
Diego Saez-Trumper
Abstract:
Measuring socioeconomic deprivation of cities in an accurate and timely fashion has become a priority for governments around the world, as the massive urbanization process we are witnessing is causing high levels of inequalities which require intervention. Traditionally, deprivation indexes have been derived from census data, which is however very expensive to obtain, and thus acquired only every…
▽ More
Measuring socioeconomic deprivation of cities in an accurate and timely fashion has become a priority for governments around the world, as the massive urbanization process we are witnessing is causing high levels of inequalities which require intervention. Traditionally, deprivation indexes have been derived from census data, which is however very expensive to obtain, and thus acquired only every few years. Alternative computational methods have been proposed in recent years to automatically extract proxies of deprivation at a fine spatio-temporal level of granularity; however, they usually require access to datasets (e.g., call details records) that are not publicly available to governments and agencies.
To remedy this, we propose a new method to automatically mine deprivation at a fine level of spatio-temporal granularity that only requires access to freely available user-generated content. More precisely, the method needs access to datasets describing what urban elements are present in the physical environment; examples of such datasets are Foursquare and OpenStreetMap. Using these datasets, we quantitatively describe neighborhoods by means of a metric, called {\em Offering Advantage}, that reflects which urban elements are distinctive features of each neighborhood. We then use that metric to {\em (i)} build accurate classifiers of urban deprivation and {\em (ii)} interpret the outcomes through thematic analysis. We apply the method to three UK urban areas of different scale and elaborate on the results in terms of precision and recall.
△ Less
Submitted 19 November, 2014;
originally announced November 2014.
-
Distributed CTL Model Checking in the Cloud
Authors:
Carlo Bellettini,
Matteo Camilli,
Lorenzo Capra,
Mattia Monga
Abstract:
The recent extensive availability of "big data" platforms calls for a more widespread adoption by the formal verification community. In fact, formal verification requires high performance data processing software for extracting knowledge from the unprecedented amount of data which come from analyzed systems. Since cloud based computing resources have became easily accessible, there is an opportuni…
▽ More
The recent extensive availability of "big data" platforms calls for a more widespread adoption by the formal verification community. In fact, formal verification requires high performance data processing software for extracting knowledge from the unprecedented amount of data which come from analyzed systems. Since cloud based computing resources have became easily accessible, there is an opportunity for verification techniques and tools to undergo a deep technological transition to exploit the new available architectures. This has created an increasing interest in parallelizing and distributing verification techniques. In this paper we introduce a distributed approach which exploits techniques typically used by the "big data" community to enable verification of Computation Tree Logic (CTL) formulas on very large state spaces using distributed systems and cloud computing facilities. The outcome of several tests performed on benchmark specifications are presented, thus showing the convenience of the proposed approach.
△ Less
Submitted 24 October, 2013;
originally announced October 2013.
-
Measuring Similarity in Large-scale Folksonomies
Authors:
Giovanni Quattrone,
Emilio Ferrara,
Pasquale De Meo,
Licia Capra
Abstract:
Social (or folksonomic) tagging has become a very popular way to describe content within Web 2.0 websites. Unlike taxonomies, which overimpose a hierarchical categorisation of content, folksonomies enable end-users to freely create and choose the categories (in this case, tags) that best describe some content. However, as tags are informally defined, continually changing, and ungoverned, social ta…
▽ More
Social (or folksonomic) tagging has become a very popular way to describe content within Web 2.0 websites. Unlike taxonomies, which overimpose a hierarchical categorisation of content, folksonomies enable end-users to freely create and choose the categories (in this case, tags) that best describe some content. However, as tags are informally defined, continually changing, and ungoverned, social tagging has often been criticised for lowering, rather than increasing, the efficiency of searching, due to the number of synonyms, homonyms, polysemy, as well as the heterogeneity of users and the noise they introduce. To address this issue, a variety of approaches have been proposed that recommend users what tags to use, both when labelling and when looking for resources.
As we illustrate in this paper, real world folksonomies are characterized by power law distributions of tags, over which commonly used similarity metrics, including the Jaccard coefficient and the cosine similarity, fail to compute. We thus propose a novel metric, specifically developed to capture similarity in large-scale folksonomies, that is based on a mutual reinforcement principle: that is, two tags are deemed similar if they have been associated to similar resources, and vice-versa two resources are deemed similar if they have been labelled by similar tags. We offer an efficient realisation of this similarity metric, and assess its quality experimentally, by comparing it against cosine similarity, on three large-scale datasets, namely Bibsonomy, MovieLens and CiteULike.
△ Less
Submitted 25 July, 2012;
originally announced July 2012.
-
Effective Retrieval of Resources in Folksonomies Using a New Tag Similarity Measure
Authors:
Giovanni Quattrone,
Licia Capra,
Pasquale De Meo,
Emilio Ferrara,
Domenico Ursino
Abstract:
Social (or folksonomic) tagging has become a very popular way to describe content within Web 2.0 websites. However, as tags are informally defined, continually changing, and ungoverned, it has often been criticised for lowering, rather than increasing, the efficiency of searching. To address this issue, a variety of approaches have been proposed that recommend users what tags to use, both when lab…
▽ More
Social (or folksonomic) tagging has become a very popular way to describe content within Web 2.0 websites. However, as tags are informally defined, continually changing, and ungoverned, it has often been criticised for lowering, rather than increasing, the efficiency of searching. To address this issue, a variety of approaches have been proposed that recommend users what tags to use, both when labeling and when looking for resources. These techniques work well in dense folksonomies, but they fail to do so when tag usage exhibits a power law distribution, as it often happens in real-life folksonomies. To tackle this issue, we propose an approach that induces the creation of a dense folksonomy, in a fully automatic and transparent way: when users label resources, an innovative tag similarity metric is deployed, so to enrich the chosen tag set with related tags already present in the folksonomy. The proposed metric, which represents the core of our approach, is based on the mutual reinforcement principle. Our experimental evaluation proves that the accuracy and coverage of searches guaranteed by our metric are higher than those achieved by applying classical metrics.
△ Less
Submitted 25 July, 2012;
originally announced July 2012.
-
State Space Exploration of RT Systems in the Cloud
Authors:
Carlo Bellettini,
Matteo Camilli,
Lorenzo Capra,
Mattia Monga
Abstract:
The growing availability of distributed and cloud computing frameworks make it possible to face complex computational problems in a more effective and convenient way. A notable example is state-space exploration of discrete-event systems specified in a formal way. The exponential complexity of this task is a major limitation to the usage of consolidated analysis techniques and tools. We present an…
▽ More
The growing availability of distributed and cloud computing frameworks make it possible to face complex computational problems in a more effective and convenient way. A notable example is state-space exploration of discrete-event systems specified in a formal way. The exponential complexity of this task is a major limitation to the usage of consolidated analysis techniques and tools. We present and compare two different approaches to state-space explosion, relying on distributed and cloud frameworks, respectively. These approaches were designed and implemented following the same computational schema, a sort of map & fold. They are applied on symbolic state-space exploration of real-time systems specified by (a timed extension of) Petri Nets, by readapting a sequential algorithm implemented as a command-line Java tool. The outcome of several tests performed on a benchmarking specification are presented, thus showing the convenience of cloud approaches.
△ Less
Submitted 30 March, 2012;
originally announced March 2012.
-
Reachability Analysis of Time Basic Petri Nets: a Time Coverage Approach
Authors:
Carlo Bellettini,
Lorenzo Capra
Abstract:
We introduce a technique for reachability analysis of Time-Basic (TB) Petri nets, a powerful formalism for real- time systems where time constraints are expressed as intervals, representing possible transition firing times, whose bounds are functions of marking's time description. The technique consists of building a symbolic reachability graph relying on a sort of time coverage, and overcomes the…
▽ More
We introduce a technique for reachability analysis of Time-Basic (TB) Petri nets, a powerful formalism for real- time systems where time constraints are expressed as intervals, representing possible transition firing times, whose bounds are functions of marking's time description. The technique consists of building a symbolic reachability graph relying on a sort of time coverage, and overcomes the limitations of the only available analyzer for TB nets, based in turn on a time-bounded inspection of a (possibly infinite) reachability-tree. The graph construction algorithm has been automated by a tool-set, briefly described in the paper together with its main functionality and analysis capability. A running example is used throughout the paper to sketch the symbolic graph construction. A use case describing a small real system - that the running example is an excerpt from - has been employed to benchmark the technique and the tool-set. The main outcome of this test are also presented in the paper. Ongoing work, in the perspective of integrating with a model-checking engine, is shortly discussed.
△ Less
Submitted 6 July, 2011;
originally announced July 2011.
