Search

Parity gamesare infinite-round two-player games played on directed graphs whose nodes are labeled with priorities. The winner of a play is determined by the smallest priority (even or odd) that is encountered infinitely often along the play. In the last two decades, several algorithms for solving parity games have been proposed and implemented in , a platform written in OCaml. includes theZielonka’s recursive algorithm(, for short) which is known to be the best performing one over random games. Notably, several attempts have been carried out with the aim of improving the performance of in , but with small advances in practice. In this work, we deeply revisit the implementation of by dealing with the use of specific data structures and programming languages such asScala,Java,C++, andGo. Our empirical evaluation shows that these choices are successful, gaining up to three orders of magnitude in running time over the classic version of the algorithm implemented in .

The term "hemp" refers to Cannabis sativa cultivars grown for industrial purposes that are characterized by lower levels of tetrahydrocannabinol (THC), the active principle responsible for Cannabis psychotropic effects. Hemp is an extraordinary crop, with enormous social and economic value, since it can be used to produce food, textiles, clothing, biodegradable plastics, paper, paint, biofuel, and animal feed, as well as lighting oil. Various parts of the hemp plant represent a valuable source of food and ingredients for nutritional supplements. While hemp inflorescence is rich in nonpsychoactive, yet biologically active cannabinoids, such as cannabidiol (CBD), which exerts potent anxiolytic, spasmolytic, as well as anticonvulsant effects, hempseed has a pleasant nutty taste and represents a valuable source of essential amino acids and fatty acids, minerals, vitamins, and fibers. In addition, hempseed oil is a source of healthy polyunsaturated fatty acids, and hemp sprouts are rich in antioxidants. This review article aims to provide a comprehensive outlook from a multidisciplinary perspective on the scientific evidence supporting hemp beneficial properties when consumed as food or supplement. Marketing of hemp-derived products is subjected to diversified and complex regulations worldwide for several reasons, including the fact that CBD is also the active principal of pharmaceutical agents and that regulatory bodies in some cases ban Cannabis inflorescence regardless of its THC content. Some key regulatory aspects of such a complex scenario are also analyzed and discussed in this review article.

Today technological innovation and digital transformation represent a concrete challenge for the transport sector, toward high quality and sustainable infrastructures and services. Within this issue, road mobility is undergoing a digital transformation based on both automation and connectivity, which promises to improve road safety, energy consumption and driving comfort, through vehicles to vehicles and vehicles to infrastructure communication and interaction (devices). The process of digital transformation for road infrastructures (and services) involves many aspects which concerns not only technological problems but also regulatory and legal aspects, both for the construction of new infrastructures (or their revamping) and for the management. Starting from these considerations, the aim of the paper was twofold: i) critically analyze the current state of practice of the Italian smart roads legislation; ii) describe the first smart road pilot project in south of Italy, the A2 Mediterranean Highway, in term of both smart technologies considered and corresponding investment costs.

We study the impact of the need for the agent to obligatorily instruct the action stop in her strategies. More specifically we consider synthesis (i.e., planning) for LTLf goals under LTL environment specifications in the case the agent must mandatorily stop at a certain point. We show that this obligation makes it impossible to exploit the liveness part of the LTL environment specifications to achieve her goal, effectively reducing the environment specifications to their safety part only. This has a deep impact on the efficiency of solving the synthesis, which can sidestep handling Buchi determinization associated to LTL synthesis, in favor of finite-state automata manipulation as in LTLf synthesis. Next, we add to the agent goal, expressed in LTLf, a safety goal, expressed in LTL. Safety goals must hold forever, even when the agent stops, since the environment can still continue its evolution. Hence the agent, before stopping, must ensure that her safety goal will be maintained even after she stops. To do synthesis in this case, we devise an effective approach that mixes a synthesis technique based on finite-state automata (as in the case of LTLf goals) and model-checking of nondeterministic Buchi automata. In this way, again, we sidestep Buchi automata determinization, hence getting a synthesis technique that is intrinsically simpler than standard LTL synthesis.

Polychlorodibenzo-p-dioxins, polychlorodibenzo-furans (PCDD/Fs) and dioxin-like polychlorobiphenyls (DL-PCBs) enter the food chain from the environment. In this study, we report the 2008-2018 time-trends in the PCDD/F and DL-PCB contamination of milk from buffaloes fed on local forage in rural areas of the Campania region. Validated according to QA/QC criteria, the dataset (N = 808 on a total of 2068 samples, after excluding follow-up results and outliers) was computed on the upper-bound value pg WHO-TEQ2005 g-1fat. We assessed time-trends and assayed baseline contamination levels, which displayed log-normal distribution. A significant decreasing trend (p < 0.01) was observed from 2008 to 2009 and 2010; the P50-P95 range fell from 2.37-8.48 pg WHO-TEQ2005 g-1fat (N = 393) in 2008 to 1.73-4.61 in 2009 (N = 86) and to 0.67-1.46 in 2010 (N = 42). From 2010 to 2018 (N = 329), no significant variation was found among years and the related dataset fitted a log-normal distribution (p < 0.05). Occurrence descriptors indicated that the baseline contamination of dairy products (mean = 0.54; P50-P95 = 0.47-1.24) in the Campania Region was well below the EU regulatory limit in force (5.5 pg WHO-TEQ2005 g-1fat). Given the Tolerable Weekly Intake of 2 pg WHO-TEQ kg-1 body weight (bw) proposed by the EFSA for PCDD/Fs and DL-PCBs, this level of baseline contamination is discussed with regard to the orientation of food safety and food security risk connected with buffalo mozzarella cheese production.

In this paper we provide a broad investigation of the symbolic approach for solving Parity Games. Specifically, we implement in a fresh tool, called Open image in new window , four symbolic algorithms to solve Parity Games and compare their performances to the corresponding explicit versions for different classes of games. By means of benchmarks, we show that for random games, even for constrained random games, explicit algorithms actually perform better than symbolic algorithms. The situation changes, however, for structured games, where symbolic algorithms seem to have the advantage. This suggests that when evaluating algorithms for parity-game solving, it would be useful to have real benchmarks and not only random benchmarks, as the common practice has been.

Parity games are abstract infinite-round games that take an important role in formal verification. In the basic setting, these games are two-player, turn-based, and played under perfect information on directed graphs, whose nodes are labeled with priorities. The winner of a play is determined according to the parities (even or odd) of the minimal priority occurring infinitely often in that play. The problem of finding a winning strategy in parity games is known to be in UPTime $\cap$ CoUPTime and deciding whether a polynomial time solution exists is a long-standing open question. In the last two decades, a variety of algorithms have been proposed. Many of them have been also implemented in a platform named PGSolver. This has enabled an empirical evaluation of these algorithms and a better understanding of their relative merits. In this paper, we further contribute to this subject by implementing, for the first time, an algorithm based on alternating automata. More precisely, we consider an algorithm introduced by Kupferman and Vardi that solves a parity game by solving the emptiness problem of a corresponding alternating parity automaton. Our empirical evaluation demonstrates that this algorithm outperforms other algorithms when the game has a a small number of priorities relative to the size of the game. In many concrete applications, we do indeed end up with parity games where the number of priorities is relatively small. This makes the new algorithm quite useful in practice.

Parity games are two-player games, played on directed graphs, whose nodes are labeled with priorities. Along a play, the maximal priority occurring infinitely often determines the winner. In the last two decades, a variety of algorithms and successive optimizations have been proposed. The majority of them have been implemented in PGSolver, written in OCaml, which has been elected by the community as the de facto platform to solve efficiently parity games as well as evaluate their performance in several specific cases. PGSolver includes the Zielonka Recursive Algorithm that has been shown to perform better than the others in randomly generated games. However, even for arenas with a few thousand of nodes (especially over dense graphs), it requires minutes to solve the corresponding game. In this paper, we deeply revisit the implementation of the recursive algorithm introducing several improvements and making use of Scala Programming Language. These choices have been proved to be very successful, gaining up to two orders of magnitude in running time.

Linear Temporal Logic (LTL) synthesis aims at automatically synthesizing a program that complies with desired properties expressed in LTL. Unfortunately it has been proved to be too difficult computationally to perform full LTL synthesis. There have been two success stories with LTL synthesis, both having to do with the form of the specification. The first is the GR(1) approach: use safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness, Generalized Reactivity(1), or GR(1). The second, inspired by AI planning, is focusing on finite-trace temporal synthesis, with LTL$$_f$$ f (LTL on finite traces) as the specification language. In this paper we take these two lines of work and bring them together. We first study the case in which we have an LTL$$_f$$ f agent goal and a GR(1) environment specification. We then add to the framework safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of LTL synthesis.

We review PLTLf and PLDLf, the pure-past versions of the well-known logics on finite traces LTLf and LDLf, respectively. PLTLf and PLDLf are logics about the past, and so scan the trace backwards from the end towards the beginning. Because of this, we can exploit a foundational result on reverse languages to get an exponential improvement, over LTLf /LDLf , for computing the corresponding DFA. This exponential improvement is reflected in several forms of sequential decision making involving temporal specifications, such as planning and decision problems in non-deterministic and non-Markovian domains. Interestingly, PLTLf (resp., PLDLf ) has the same expressive power as LTLf (resp., LDLf ), but transforming a PLTLf (resp., PLDLf ) formula into its equivalent LTLf (resp.,LDLf) is quite expensive. Hence, to take advantage of the exponential improvement, properties of interest must be directly expressed in PLTLf /PLDLf .

We introduce Dynamic Escape Game (DEC), a tool that provides emergency evacuation plans in situations where some of the escape paths may become unavailable at runtime. We formalize the setting as a reachability two-player turn-based game where the universal player has the power of inhibiting at runtime some moves to the existential player. Thus, the universal player can change the structure of the game arena along a play. DEC uses a graphical interface to depict the game and displays a winning play whenever it exists.