Abstract
Context-free languages are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma for Context-Free Languages states a property that is valid for all context-free languages, which makes it a tool for showing the existence of non-context-free languages. This paper presents a formalization, extending the previously formalized Lemma, of the fact that several well-known languages are not context-free. Moreover, we build on those results to construct a formal proof of the well-known property that context-free languages are not closed under intersection. All the formalization has been mechanized in the Coq proof assistant.

Abstract
Emerging markets contain the vast majority of the world's population. Despite the enormous number of inhabitants, these markets still lack a proper finance infrastructure. One of the main difficulties felt by customers is the access to loans. This limitation arises from the fact that most customers usually lack a verifiable credit history. As such, traditional banks are unable to provide loans. This paper proposes credit scoring modeling based on non-traditional-data, acquired from smartphones, for loan classification processes. We use Logistic Regression (LR) and Support Vector Machine (SVM) models which are the top linear models in traditional banking. Then we compared the transformation of the training datasets creating boolean indicators against the categorization using Weight of Evidence (WoE). Our models surpassed the performance of the manual loan application selection process, improving the approval rate and decreasing the overdue rate. Compared to the baseline, the loans approved by meeting the criteria of the SVM model presented a decreased overdue rate. At the same time, using the score generated by a SVM model we were able to grant more loans. This paper shows that credit scoring can be useful in emerging markets. The non-traditional data can be used to build robust algorithms that can identify good borrowers as in traditional banking.

Abstract
Petri nets play a central role in the formal modelling of a wide range of complex systems and scenarios. Their ability to handle with both concurrency and resource awareness justifies their spread in the current formal development practices. On the logic side, Dynamic Logics are widely accepted as the de facto formalisms to reason about computational systems. However, as usual, the application to new situations raises new challenges and issues. The ubiquity of failures in the execution of current systems, interpreted in these models as triggered events that are not followed by the corresponding transition, entails not only the adjustment of these structures to deal with this reality, but also the introduction of new logics adequate to this emerging phenomenon. This paper contributes to this challenge by exploring a combination of two previous works of the authors, namely the Propositional Dynamic Logic for Petri Nets [1] and a parametric construction of multi-valued dynamic logics presented in [13]. This exercise results in a new family of Dynamic Logics for Petri Nets suitable to deal with firing failures. © 2019, IFIP International Federation for Information Processing.

Abstract

Abstract
Long-term, regular, grid-aware participants are one of the cornerstones of demand management activities that provide grid services. However, voluntary participation to demand management activities is still at low rates, while most customers are not sufficiently aware of the management potential of their flexible loads. Smart metering and data post-processing play a vital role in demand management programs to visualize consumption profiles, highlight flexibility potential and evaluate load management performance of customers. Additionally, gamification techniques can be employed to motivate users to achieve behavioral changes in their consumption profiles, providing financial and social incentives. Long-term field demonstrations and exploration of detailed evaluation metrics have been the main gaps in this area of study. This paper presents and discusses the results of a 13-month field demonstration of a gamified residential demand management platform. 4-month monitoring period is followed by a 9-month gamification period in four houses in Istanbul, Turkey. © 2019 IEEE.

Abstract