Author name cluster

Michele Chiari

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

1 author row

I&C Journal 2025 Journal Article

Cyclic operator precedence grammars for parallel parsing

Michele Chiari
Dino Mandrioli
Matteo Pradella

Operator precedence languages (OPLs) enjoy the local parsability property, which means that a code fragment enclosed within a pair of markers playing the role of parentheses can be parsed with no knowledge of its external context. This property has been exploited to build parallel parsers for languages formalized as OPLs. It has been observed, however, that when the syntax trees of sentences have a linear substructure, parsing must necessarily proceed sequentially, making it ineffective to split such a subtree into chunks to be processed in parallel. This inconvenience derives from the hypothesis that the equality precedence relation cannot be cyclic, which has been so far assumed by most literature on OPLs. This hypothesis was motivated by the need to keep the mathematical notation as simple as possible, although it caused a discrepancy between the expressive power of operator precedence grammars and other formalisms defining OPLs such as operator precedence automata, monadic second order logic and operator precedence expressions, which do not assume acyclicity. We present an enriched version of operator precedence grammars, called cyclic, that allows for a simplified version of regular expressions in the right hand sides of grammar rules. For this class of operator precedence grammars the acyclicity hypothesis of the equality precedence relation is no more needed to guarantee the algebraic properties of the generated languages. The expressive power of the cyclic grammars is now fully equivalent to that of other formalisms defining OPLs. As a result, cyclic operator precedence grammars produce unranked syntax trees and sentences with flat unbounded substructures that can be naturally partitioned into chunks suitable for parallel parsing.

Details DOI

AAMAS Conference 2025 Conference Paper

Decentralized Planning Using Probabilistic Hyperproperties

Francesco Pontiggia
Filip Macák
Roman Andriushchenko
Michele Chiari
Milan Češka

Multi-agent planning under stochastic dynamics is usually formalised using decentralized (partially observable) Markov decision processes (MDPs) and reachability or expected reward specifications. In this paper, we propose a different approach: we use an MDP describing how a single agent operates in an environment and probabilistic hyperproperties to capture desired temporal objectives for a set of decentralized agents operating in the environment. We extend existing approaches for model checking probabilistic hyperproperties to handle temporal formulae relating paths of different agents, thus requiring the self-composition between multiple MDPs. Using several case studies, we demonstrate that our approach provides a flexible and expressive framework to broaden the specification capabilities with respect to existing planning techniques. Additionally, we establish a close connection between a subclass of probabilistic hyperproperties and planning for a particular type of Dec-MDPs, for both of which we show undecidability. This lays the ground for the use of existing decentralized planning tools in the field of probabilistic hyperproperty verification.

PDF

TCS Journal 2020 Journal Article

Operator precedence temporal logic and model checking

Michele Chiari
Dino Mandrioli
Matteo Pradella

In the last decades much research effort has been devoted to extending the success of model checking from the traditional field of finite state machines and various versions of temporal logics to suitable subclasses of context-free languages and appropriate extensions of temporal logics. To the best of our knowledge such attempts only covered structured languages, i. e. languages whose structure is immediately “visible” in their sentences, such as tree-languages or visibly pushdown ones. In this paper we present a new temporal logic suitable to express and automatically verify properties of operator precedence languages. This “historical” language family has been recently proved to enjoy fundamental algebraic and logic properties that make it suitable for model checking applications yet breaking the barrier of visible-structure languages (in fact the original motivation of its inventor Floyd was just to support efficient parsing, i. e. building the “hidden syntax tree” of language sentences). We prove that our logic is at least as expressive as analogous logics defined for visible pushdown languages yet covering a much more powerful family; we design a procedure that, given a formula in our logic builds an automaton recognizing the sentences satisfying the formula, whose size is at most exponential in the length of the formula. Our results cover both finite and infinite string languages.

Details DOI

GandALF Workshop 2018 Workshop Paper

Temporal Logic and Model Checking for Operator Precedence Languages

Michele Chiari
Dino Mandrioli
Matteo Pradella

In the last decades much research effort has been devoted to extending the success of model checking from the traditional field of finite state machines and various versions of temporal logics to suitable subclasses of context-free languages and appropriate extensions of temporal logics. To the best of our knowledge such attempts only covered structured languages, i. e. languages whose structure is immediately "visible" in their sentences, such as tree-languages or visibly pushdown ones. In this paper we present a new temporal logic suitable to express and automatically verify properties of operator precedence languages. This "historical" language family has been recently proved to enjoy fundamental algebraic and logic properties that make it suitable for model checking applications yet breaking the barrier of visible-structure languages (in fact the original motivation of its inventor Floyd was just to support efficient parsing, i. e. building the "hidden syntax tree" of language sentences). We prove that our logic is at least as expressive as analogous logics defined for visible pushdown languages yet covering a much more powerful family; we design a procedure that, given a formula in our logic builds an automaton recognizing the sentences satisfying the formula, whose size is at most exponential in the length of the formula.

PDF Details DOI