1,721,107 research outputs found
Teoria degli automi per linguaggi formali
Full text linkL'esigenza di caratterizzare proprietà di sequenze di simboli è un problema comune ad un'ampia varietà di settori, dalla linguistica alla biologia computazionale, passando per molteplici campi dell'informatica, dall'interpretazione del software da parte del calcolatore alla verifica di correttezza dei sistemi di calcolo e reti di computer. Una tale variet`a nasce dall'interpretazione che si può dare dei simboli, che possono rappresentare termini di un linguaggio naturale, molecole, istruzioni di un linguaggio di programmazione, segnali digitali, messaggi di un protocollo di comunicazione o altri eventi.Lo studio rigoroso di questo problema generale può essere affrontato da due punti di vista che vedremo essere ortogonali. Da una parte, possiamo caratterizzare le sequenze di simboli come espressioni di un linguaggio generate attraverso le regole di una grammatica formale. Dall'altra, possiamo immaginare di definire una macchina astratta, comunemente detta automa, che ha l'obiettivo di riconoscere il linguaggio descritto da tali sequenze. Per via della vastità di questi argomenti, scopo del presente lavoro è introdurre il secondo di questi approcci formali, senza perdere di vista il legame forte che esiste con il primo
On the Modeling and Verification of Collective and Cooperative Systems
Full text linkThe formal description and verification of networks of cooperative and interacting agents is made difficult by the interplay of several different behavioral patterns, models of communication, scalability issues. In this paper, we will explore the functionalities and the expressiveness of a general-purpose process algebraic framework for the specification and model checking based analysis of collective and cooperative systems. The proposed syntactic and semantic schemes are general enough to be adapted with small modifications to heterogeneous application domains, like, e.g., crowdsourcing systems, trustworthy networks, and distributed ledger technologies
Quantitative Aspects of Programming Languages and Systems over the past 2^4 years and beyond
Full text linkQuantitative aspects of computation are related to the use of both physical and mathematical quantities, including time, performance metrics, probability, and measures for reliability and security. They are essential in characterizing the behaviour of many critical systems and in estimating their properties. Hence, they need to be integrated both at the level of system modeling and within the verification methodologies and tools. Along the last two decades a variety of theoretical achievements and automated techniques have contributed to make quantitative modeling and verification mainstream in the research community. In the same period, they represented the central theme of the series of workshops entitled Quantitative Aspects of Programming Languages and Systems (QAPL) and born in 2001. The aim of this survey is to revisit such achievements and results from the standpoint of QAPL and its community
A Framework Balancing Privacy and Cooperation Incentives in User-Centric Networks
Full text linkUser-centricity subsumes new models of Internet connectivity
and resource sharing, which are based on collaborative
behaviors asking for cooperation strategies. On one hand, typical
incentives stimulating cooperation, based, e.g., on trust and
remuneration, require some level of information disclosure that
can be used to outline the user behavior. On the other hand,
disclosing such information can be considered as a privacy breach
keeping the users from being involved in certain interactions. In
this paper, we present a flexible privacy-preserving mechanism
trading privacy for trust-based and cost-based incentives. Firstly,
the proposed mechanism is validated theoretically through model
checking based analysis. Secondly, implementation issues are
discussed with respect to the design of ad-hoc solutions based on
a centralized reputation system and a distributed trust system
On the modeling and verification of the spread of fake news, algebraically
No full textIn recent years, one of the major issues concerning the study of online social network phenomena is related to the diffusion of misinformation, commonly known as fake news. In the literature, several mathematical tools are used to investigate both the identifying attributes of fake news and their spreading model. This work concentrates on the latter aspect and follows the lines of research inspired by the analysis of epidemic models. Its main contribution is the definition of a modeling framework based on process algebra for the explicit, formal representation of typical behavioral patterns of agents in social networks, and the use of a probabilistic verification framework based on modal logics and model checking for the quantitative analysis of the fake news spread
Saving Privacy in Trust-Based User-Centric Distributed Systems
No full textUser-centricity is a design philosophy subsuming new models of Internet connectivity and resource sharing, whose development is mainly driven by what users offer and require. To promote user-centric services and collaborative behaviors, incentives are needed that are typically based on trust relations and remuneration. In this paper, we show that privacy-preserving mechanisms can favor user's involvement if privacy can be traded with trust and cost. In particular, we present and evaluate formally a model ensuring an adequate level of flexibility among privacy, trust, and cost in the setting of distributed systems
Formal Approach to Design and Automatic Verification of Cooperation-Based Networks
Full text linkThe efficacy and efficiency of cooperation incentives in user-centric networks is a challenging issue that involves tradeoff among trust, social, and economic aspects. Two well-established approaches to stimulate resource sharing and cooperation rely on reputation and remuneration, the complementary functioning of which shall increase users' motivation and discourage mistrust and selfishness. In order to verify the benefits of the joint application of these mechanisms, we specify and analyze formally a recently proposed cooperation model by employing tool-supported probabilistic model checking techniques
Design and Verification of Trusted Collective Adaptive Systems
Full text linkCollective adaptive systems (CAS) often adopt cooperative operating strategies to run distributed decision-making mechanisms. Sometimes, their effectiveness massively relies on the collaborative nature of individuals’ behavior. Stimulating cooperation while preventing selfish and malicious behaviors is the main objective of trust and reputation models. These models are largely used in distributed, peer-to-peer environments and, therefore, represent an ideal framework for improving the robustness, as well as security, of CAS. In this article, we propose a formal framework for modeling and verifying trusted CAS. From the modeling perspective, mobility, adaptiveness, and trust-based interaction represent the main ingredients used to define a flexible and easy-to-use paradigm. Concerning analysis, formal automated techniques based on equivalence and model checking support the prediction of the CAS behavior and the verification of the underlying trust and reputation models, with the specific aim of estimating robustness with respect to the typical attacks conducted against webs of trust
Modeling and verification of trust and reputation systems
Full text linkTrust is a basic soft-security condition influencing interactive and
cooperative behaviors in online communities. Several systems and models have
been proposed to enforce and investigate the role of trust in the process of
favoring successful cooperations while minimizing selfishness and failure.
However, the analysis of their effectiveness and efficiency is a challenging
issue. This paper provides a formal approach to the design and verification of
trust infrastructures used in the setting of software architectures and computer
networks supporting online communities. The proposed framework encompasses a
process calculus of concurrent systems, a temporal logic for trust, and model
checking techniques. Both functional and quantitative aspects can be modeled and
analyzed, while several types of trust models can be integrated
- …
