CySource has developed an AI based SaaS cyber education platform providing large scale human capital transformation

CYSOURCE

This paper is available on arxiv under CC BY-SA 4.0 DEED license. Authors: (1) Tomáš Jakl, Czech Academy of Sciences and Czech Technical University; (2) Dan Marsden, School of Computer Science University of Nottingham; (3) Nihil Shah, Department of Computer Science University of Oxford. Table of Links Abstract & Introduction Prelimenaries FVM Theorems for Positive Existential Fragments FVM Theorems for Counting Logic FVM Theorems for The Full Logic Abstract FVM Theorems for Products Adding Equality and Other Enrichment Conclusions, Acknowledgments & References Appendix A FVM theorems for coproducts Appendix B Proofs Omitted from Section III Appendix C Proofs Omitted from Section IV Appendix D Proofs Omitted from Section V Appendix E Proofs Omitted from Section VI Appendix F Proofs Omitted from Section VII VIII. CONCLUSION We presented a categorical approach to the composition method, and specifically Feferman–Vaught–Mostowski theorems. We exploit game comonads to encapsulate the logics and their model comparison games. Surprising connections to classical constructions in category theory, and especially the monad theory of bilinear maps emerged from this approach, cf. Section V-A. For finite model theorists, our work provides a novel highlevel account of many FVM theorems, abstracting away from individual logics and constructions. Furthermore, concrete instances of these theorems are verified purely semantically, by finding a suitable collection homomorphisms forming a Kleisli law satisfying (S2’), instead of the usual delicate verification that strategies of model comparison games compose. For game comonads, we provide a much needed tool that enables us to handle logical relationships between structures as they are transformed or viewed in terms of different logics. The FVM results in this paper, combined with judicious use of the techniques described in Section VII can be pushed significantly further. FVM theorems and the compositional method are of particular significance in the setting of monadic second-order (MSO) logic [49]. Exploiting the results we have presented for the composition method, a follow up paper will give a comonadic semantics for MSO, and develop a semantic account of Courcelle’s algorithmic meta-theorems [5]. The original theorem of Feferman–Vaught [3] is very flexible, including incorporating structure on the indices of families of models to be combined by an operation, as well as the models themselves. This aspect is currently outside the scope of our comonadic methods. An ad-hoc adaptation of our approach also gives a proof of the FVM theorem for free amalgamations, but this does not follow directly from our theorems. Developing these extensions is left to future work. The present work bears some resemblance to Turi and Plotkin’s bialgebraic semantics [50], a categorical model of structural operational semantics (SOS) [51]. Turi and Plotkin noticed that the SOS rules assigning behaviour to syntax could be abstracted as a certain distributive law λ. An algebra encodes the composition operations of the syntax, and a coalgebra the behaviour. If this pair is suitably compatible with λ, forming a so-called λ-bialgebra, then crucially bisimulation is a congruence with respect to the composition operations. Both bialgebraic semantics and our work presented in this paper give a categorical account of well-behaved composition operations, with the interaction between composition and observable behaviour mediated by some form of distributive law. There are also essential differences: bialgebraic semantics typically focuses on assigning behaviour to syntax, whereas FVM theorems encompass operations on models. Our FVM theorems are parametric in a choice of logic or observable behaviour, while the notion of bisimulation in bialgebraic semantics is fixed by the coalgebra signature functor. The natural presence of positive existential and counting quantifier variants of FVM theorems, and the incorporation of resource parameters, do not seem to have a direct analogue in bialgebraic semantics. The similarities are intriguing, and exploring the relationship between bialgebraic semantics and our approach to FVM theorems is left to future work. We would like to thank Clemens Berger for suggesting the connection with parametric adjoints and Nathanael Arkor for his suggestions on terminology. We are also grateful to the members of the EPSRC project “Resources and co-resources” for their feedback. Acknowledgements: REFERENCES [1] L. Libkin, Elements of finite model theory. Springer, 2004, vol. 41. [2] A. Mostowski, “On direct products of theories,” The Journal of Symbolic Logic, vol. 17, no. 1, pp. 1–31, 1952. [3] S. Feferman and R. L. Vaught, “The first-order properties of algebraic systems,” Fundamenta Mathematicae, vol. 47, 1959. [4] J. A. Makowsky, “Algorithmic uses of the Feferman–Vaught theorem,” Annals of Pure and Applied Logic, vol. 126, no. 1-3, pp. 159–213, 2004. [5] B. Courcelle and J. Engelfriet, Graph structure and monadic secondorder logic: a language-theoretic approach. Cambridge University Press, 2012, vol. 138. [6] A. Ehrenfeucht, “An application of games to the completeness problem for formalized theories,” Fundamenta mathematicae, vol. 49, no. 129- 141, p. 13, 1960. [7] R. Fraïssé, “Sur quelques classifications des relations, basées sur des isomorphismes restreints,” Publications Scientifiques de l’Université d’Alger. Série A (mathématiques), vol. 2, pp. 273–295, 1955. [8] P. G. Kolaitis and M. Y. Vardi, “Infinitary logics and 0–1 laws,” Information and computation, vol. 98, no. 2, pp. 258–294, 1992. [9] M. Hennessy and R. Milner, “On observing nondeterminism and concurrency,” in International Colloquium on Automata, Languages, and Programming. Springer, 1980, pp. 299–309. [10] S. Abramsky, A. Dawar, and P. Wang, “The pebbling comonad in finite model theory,” in 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. IEEE Computer Society, 2017, pp. 1–12. [11] S. Abramsky and N. Shah, “Relating structure and power: Comonadic semantics for computational resources,” Journal of Logic and Computation, vol. 31, no. 6, pp. 1390–1428, 2021. [12] E. Moggi, “Computational lambda-calculus and monads,” in Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS ’89), Pacific Grove, California, USA, June 5-8, 1989. IEEE Computer Society, 1989, pp. 14–23. [13] ——, “Notions of computation and monads,” Information and Computation, vol. 93, no. 1, pp. 55–92, 1991. [14] E. G. Manes, Algebraic theories. Springer Science, 1976, vol. 26. [15] S. Abramsky and D. Marsden, “Comonadic semantics for guarded fragments,” in 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. IEEE, 2021, pp. 1–13. [16] A. Ó. Conghaile and A. Dawar, “Game comonads & generalised quantifiers,” in 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference), ser. LIPIcs, C. Baier and J. Goubault-Larrecq, Eds., vol. 183. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021, pp. 16:1–16:17. [17] Y. Montacute and N. Shah, “The pebble-relation comonad in finite model theory,” in LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, C. Baier and D. Fisman, Eds. ACM, 2022, pp. 13:1–13:11. [Online]. Available: https://doi.org/10.1145/3531130.3533335 [18] T. Paine, “A pebbling comonad for finite rank and variable logic, and an application to the equirank-variable homomorphism preservation theorem,” in Proceedings of the 36th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2020, Online, October 1, 2020, ser. Electronic Notes in Theoretical Computer Science, P. Johann, Ed., vol. 352. Elsevier, 2020, pp. 191–209. [19] A. Dawar, T. Jakl, and L. Reggio, “Lovász-type theorems and game comonads,” in 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. IEEE, 2021, pp. 1–13. [20] S. Abramsky and D. Marsden, “Comonadic semantics for hybrid logic,” in 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria, ser. LIPIcs, S. Szeider, R. Ganian, and A. Silva, Eds., vol. 241. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, pp. 7:1–7:14. [21] L. Reggio, “Polyadic sets and homomorphism counting,” Advances in Mathematics, vol. 410, p. 108712, 2022. [22] S. Abramsky, “Structure and power: an emerging landscape,” Fundam. Informaticae, vol. 186, no. 1-4, pp. 1–26, 2022. [23] S. Abramsky and L. Reggio, “Arboreal categories and resources,” in 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), ser. LIPIcs, N. Bansal, E. Merelli, and J. Worrell, Eds., vol. 198. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021, pp. 115:1–115:20. [24] H. Ebbinghaus and J. Flum, Finite model theory, ser. Perspectives in Mathematical Logic. Springer, 1995. [25] E. G. Manes and P. Mulry, “Monad compositions I: general constructions and recursive distributive laws,” Theory and Applications of Categories, vol. 18, no. 7, pp. 172–208, 2007. [26] A. Kock, “Bilinearity and cartesian closed monads,” Mathematica Scandinavica, vol. 29, no. 2, pp. 161–174, 1971. [27] T. Jakl, D. Marsden, and N. Shah, “Generalizations of bilinear maps,” 2022, technical report, arXiv preprint. [Online]. Available: https://arxiv.org/abs/2205.05382 [28] A. Dawar, S. Severini, and O. Zapata, “Pebble games and cospectral graphs,” Electronic Notes in Discrete Mathematics, vol. 61, pp. 323– 329, 2017. [29] S. Abramsky and N. Tzevelekos, “Introduction to categories and categorical logic,” in New structures for physics. Springer, 2010, pp. 3–94. [30] S. Awodey, Category theory. Oxford University Press, 2010. [31] C. Stirling, Modal and temporal properties of processes. Springer Science & Business Media, 2001. [32] A. W. Roscoe, Understanding concurrent systems. Springer Science & Business Media, 2010. [33] H. Kleisli, “Every standard construction is induced by a pair of adjoint functors,” Proceedings of the American Mathematical Society, vol. 16, no. 3, pp. 544–546, 1965. [34] B. Jacobs, “Semantics of weakening and contraction,” Annals of Pure and Applied Logic, vol. 69, no. 1, pp. 73–106, 1994. [35] S. Abramsky, T. Jakl, and T. Paine, “Discrete density comonads and graph parameters,” in Coalgebraic Methods in Computer Science - 16th IFIP WG 1.3 International Workshop, CMCS 2022, Colocated with ETAPS 2022, Munich, Germany, April 2-3, 2022, Proceedings, ser. Lecture Notes in Computer Science, H. H. Hansen and F. Zanasi, Eds., vol. 13225. Springer, 2022, pp. 23–44. [Online]. Available: https://doi.org/10.1007/978-3-031-10736-8_2 [36] P. T. Johnstone, “Adjoint lifting theorems for categories of algebras,” Bulletin of the London Mathematical Society, vol. 7, no. 3, pp. 294– 297, 1975. [37] A. Kock, “Closed categories generated by commutative monads,” Journal of the Australian Mathematical Society, vol. 12, no. 4, pp. 405–424, 1971. [38] G. Seal, “Tensors, monads and actions,” Theory and Applications of Categories, vol. 28, no. 15, pp. 403–434, 2013. [39] F. E. Linton, “Coequalizers in categories of algebras,” in Seminar on triples and categorical homology theory. Springer, 1969, pp. 75–90. [40] R. Street, “The petit topos of globular sets,” Journal of Pure and Applied Algebra, vol. 154, no. 1-3, pp. 299–315, 2000. [41] M. Weber, “Generic morphisms, parametric representations and weakly cartesian monads,” Theory and Applications of Categories, vol. 13, no. 14, pp. 191–234, 2004. [42] ——, “Familial 2-functors and parametric right adjoints,” Theory and Applications of Categories, vol. 18, no. 22, pp. 665–732, 2007. [43] C. Berger, P.-A. Mellies, and M. Weber, “Monads with arities and their associated theories,” Journal of Pure and Applied Algebra, vol. 216, no. 8-9, pp. 2029–2048, 2012. [44] T. Altenkirch, J. Chapman, and T. Uustalu, “Monads need not be endofunctors,” in International Conference on Foundations of Software Science and Computational Structures. Springer, 2010, pp. 297–311. [45] P. J. Freyd and G. M. Kelly, “Categories of continuous functors, I,” Journal of Pure and Applied Algebra, vol. 2, no. 3, pp. 169–191, 1972. [46] B. Bednarczyk and M. Urbanczyk, “Comonadic semantics for description logics games,” in Proceedings of the 35th International Workshop on Description Logics (DL 2022) co-located with Federated Logic Conference (FLoC 2022), Haifa, Israel, August 7th to 10th, 2022, ser. CEUR Workshop Proceedings, O. Arieli, M. Homola, J. C. Jung, and M. Mugnier, Eds., vol. 3263. CEUR-WS.org, 2022. [Online]. Available: http://ceur-ws.org/Vol-3263/paper-5.pdf [47] M. Bojanczyk, “Separator logic and star-free expressions ´ for graphs,” 2021, arXiv preprint. [Online]. Available: https://arxiv.org/abs/2107.13953 [48] N. Schirrmacher, S. Siebertz, and A. Vigny, “First-Order Logic with Connectivity Operators,” in 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), ser. Leibniz International Proceedings in Informatics (LIPIcs), F. Manea and A. Simpson, Eds., vol. 216. Dagstuhl, Germany: Schloss Dagstuhl – LeibnizZentrum für Informatik, 2022, pp. 34:1–34:17. [Online]. Available: https://drops.dagstuhl.de/opus/volltexte/2022/15754 [49] Y. Gurevich, “Monadic second-order theories,” in Model-theoretic logics, J. Barwise and S. Feferman, Eds. Cambridge University Press, 1985, pp. 479–506. [50] D. Turi and G. Plotkin, “Towards a mathematical operational semantics,” in Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science. IEEE, 1997, pp. 280–291. [51] G.D.Plotkin, “A structural approach to operational semantics,” Aarhus University, Tech. Rep. DAIMI FN-19, 1981. [52] J. Adámek, J. Adamek, J. Rosicky et al., Locally presentable and accessible categories. Cambridge University Press, 1994, vol. 189.

A Categorical Account of
Composition Methods in Logic: Conclusions, Acknowledgments & References

This paper is available on arxiv under CC BY-SA 4.0 DEED license. Authors: (1) Tomáš Jakl, Czech Academy of Sciences and Czech Technical University; (2) Dan Marsden, School of Computer Science University of Nottingham; (3) Nihil Shah, Department of Computer Science University of Oxford. Table of Links Abstract & Introduction Prelimenaries FVM Theorems for Positive Existential Fragments FVM Theorems for Counting Logic FVM Theorems for The Full Logic Abstract FVM Theorems for Products Adding Equality and Other Enrichment Conclusions, Acknowledgments & References Appendix A FVM theorems for coproducts Appendix B Proofs Omitted from Section III Appendix C Proofs Omitted from Section IV Appendix D Proofs Omitted from Section V Appendix E Proofs Omitted from Section VI Appendix F Proofs Omitted from Section VII Abstract We present a categorical theory of the composition methods in finite model theory – a key technique enabling modular reasoning about complex structures by building them out of simpler components. The crucial results required by the composition methods are Feferman–Vaught–Mostowski (FVM) type theorems, which characterize how logical equivalence behaves under composition and transformation of models. Our results are developed by extending the recently introduced game comonad semantics for model comparison games. This level of abstraction allow us to give conditions yielding FVM type results in a uniform way. Our theorems are parametric in the classes of models, logics and operations involved. Furthermore, they naturally account for the positive existential fragment, and extensions with counting quantifiers of these logics. We also reveal surprising connections between FVM type theorems, and classical concepts in the theory of monads. We illustrate our methods by recovering many classical theorems of practical interest, including a refinement of a previous result by Dawar, Severini, and Zapata concerning the 3-variable counting logic and cospectrality. To highlight the importance of our techniques being parametric in the logic of interest, we prove a family of FVM theorems for products of structures, uniformly in the logic in question, which cannot be done using specific game arguments. I. INTRODUCTION Composition methods constitute a family of techniques in finite model theory for understanding the logical properties of complex structures [1]. One works in a modular fashion, building a structure out of simpler components. The larger structure can then be understood in terms of the logical properties of its parts, and how they behave under the operations used in the construction The first result of this type was proved by Mostowski [2], who showed that the first-order theory of the product of two structures A×B is determined by the first-order theories of A and B. Later, Feferman and Vaught famously proved a very general result for first-order logic, which included showing that the same holds true for infinite products and infinite disjoint unions of structures of the same type [3]. Since then many more Feferman–Vaught–Mostowski (FVM) theorems1 have been shown for various operations, logics and types of structures. These theorems have important applications in the theory of algorithms [4], for example in the development of algorithmic meta-theorems such as Courcelle’s theorem [5]. For our purposes, the typical form of an FVM theorem for a fixed n-ary operation H and logics is as follows. Given structures and L1, . . . , Ln+1 A1, . . . , An B1, . . . , Bn, Here denotes equivalence with respect to the logic . Typically, is either one or two. For example, writing ≡F O for equivalence in first-order logic, Mostowski’s result is given in the form of (1) as: ≡L L n A key tool in finite model theory for establishing that two structures are logically equivalent is that of a model comparison game. Examples of such games are the Ehrenfeucht– Fraïssé [6], [7], pebbling [8] and bisimulation games [9], establishing equivalence in fragments of first order and modal logic. FVM theorems are typically proven using these games, building a winning strategy for the composite structure out of winning strategies for the components. Despite their usefulness, working with model comparison games often requires intricate combinatorial arguments that have to be carefully adapted with even the slightest change of problem domain. To mitigate the difficulty with using game arguments directly, finite model theorists introduced higherlevel methods such as locality arguments or 0–1 laws to establish model equivalences or inexpressibility. The recently introduced game comonad framework [10], [11] provides a new such tool. This provides a unifying formalism for reasoning about model comparison games, using categorical methods. The definition of a comonad enables a transfer of results from the formally dual theory of monads, commonly encountered in the categorical semantics of computation and universal algebra [12], [13], [14]. Game comonads are designed to encapsulate a particular model comparison game, and are the key abstraction allowing us to give uniform results, whilst avoiding making arguments specific to a particular logic or its corresponding game. The early work on game comonads focused on capturing many important logics [15], [16], [17], laying the foundations for further developments. More recent results recover classical theorems from finite model theory, as well as completely new results [18], [19], [20], [21]. See [22] for a recent survey and [23] for an axiomatic formulation. Until now, there has been no account of the composition method with the game comonad framework. We close this gap by introducing a novel method for proving FVM theorems within the game comonad approach, giving results uniformly in the classes of structures, operations and logics involved. Instantiating the abstract results for our example game comonads yields concrete FVM theorems with respect to three typical fragments of first-order logic: the positive existential fragment, i.e. the fragment of firstorder logic of formulas not using universal quantification or negations, counting logic, i.e. the extension of first-order logic with counting quantifiers, full first-order logic. Conventionally, proving an FVM theorem involves cleverly combining several winning model-comparison game strategies to form a winning strategy on the composite structures. In our game comonads approach, we only need to find a collection of morphisms of a specified form to obtain an FVM theorem for the positive existential logic. This collection of morphisms is a formal witness to a combination of strategies. Perhaps surprisingly, to witness equivalence in the counting logic, the same collection of morphisms only has to satisfy two additional axioms which coincide with the standard definition of Kleisli law [25]. Although of practical interest, the FVM theorems in Sections III and IV are relatively straightforward to prove. We present them in detail for pedagogical reasons to develop the ideas gradually. The abstract FVM theorem for the full fragment is more technically challenging. This theorem shows that two additional assumptions suffice to extend an FVM theorem from counting logic to the full logic. We can rephrase these assumptions categorically as showing the operation lifts to a parametric relative right adjoint over an appropriate category. Surprising connections arise with classical results in monad theory, generalizing the notion of bilinear map and its classifying tensor product from ordinary linear algebra [26], [27].

A Categorical Account of
Composition Methods in Logic: Abstract & Introduction

This paper is available on arxiv under CC BY-NC-SA 4.0 DEED license. Authors: (1) Pascal Baumann, Max Planck Institute for Software Systems (MPI-SWS), Germany; (2) Rupak Majumdar, Max Planck Institute for Software Systems (MPI-SWS), Germany; (3) Ramanathan S. Thinniyam, Max Planck Institute for Software Systems (MPI-SWS), Germany; (4) Georg Zetzsche, Max Planck Institute for Software Systems (MPI-SWS), Germany. Table of Links Introduction Dynamic Networks of Concurret Pushdown Systems (DCPS) Warm-up: Non-Termination Fair Non-Termination From Progressive Runs for VASSB to Reachability Starvation Conclusion, Acknowledgment & References A. Strengthening Fairness to Progressive Runs B. Proofs from Section 4.1 C. Proofs for Section 5 D. Proofs for Section 5.3 E. Proofs for Section 6 7 CONCLUSION ACKNOWLEDGMENTS This research was sponsored in part by the Deutsche Forschungsgemeinschaft project 389792660 TRR 248–CPEC and by the European Research Council under the Grant Agreement 610150 (http://www.impact-erc.eu/) (ERC Synergy Grant ImPACT). REFERENCES Parosh Aziz Abdulla, Karlis Čer ¯ ans, Bengt Jonsson, and Yih-Kuen Tsay. 1996. General decidability theo ¯ rems for infinitestate systems. In Proceedings of the Eleventh Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, 313–321. Krzysztof R. Apt and Ernst-Rüdiger Olderog. 1991. Verification of Sequential and Concurrent Programs. Springer-Verlag. Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, and Akash Lal. 2012a. Detecting Fair Non-termination in Multithreaded Programs. In Proceedings of CAV 2012. 210–226. https://doi.org/10.1007/978-3-642-31424-7_19 Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. 2012b. Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding. In Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings (Lecture Notes in Computer Science), Vol. 7561. Springer, 152–166. Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. 2017. Parity Games on Bounded Phase Multi-pushdown Systems. In Networked Systems - 5th International Conference, NETYS 2017, Marrakech, Morocco, May 17-19, 2017, Proceedings (Lecture Notes in Computer Science), Vol. 10299. Springer, 272–287. Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer. 2009. Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. In Proceedings of TACAS 2009. 107–123. Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer. 2011. Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads. Log. Methods Comput. Sci. 7, 4 (2011). https://doi.org/10.2168/LMCS-7(4:4)2011 Georg Bachmeier, Michael Luttenberger, and Maximilian Schlund. 2015. Finite Automata for the Sub- and Superword Closure of CFLs: Descriptional and Computational Complexity. In 9th International Conference on Language and Automata Theory and Applications, LATA 2015, Nice, France, March 2-6, 2015, Proceedings. Springer, 473–485. Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. 2020. The Complexity of Bounded Context Switching with Dynamic Thread Creation. In 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference) (LIPIcs), Vol. 168. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 111:1–111:16. Julius Richard Büchi. 1964. Regular canonical systems. Archiv für mathematische Logik und Grundlagenforschung 6, 3-4 (1964), 91–111. Heino Carstensen. 1987. Decidability questions for fairness in Petri nets. In Proceedings of STACS 1987. Springer, 396–407. Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2007. Proving thread termination. In Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007. ACM, 320–330. Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2011. Proving program termination. Commun. ACM 54, 5 (2011), 88–98. https://doi.org/10.1145/1941487.1941509 Bruno Courcelle. 1991. On construction obstruction sets of words. EATCS 44 (1991), 178–185. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. 2019. The reachability problem for Petri nets is not elementary. In Proceedings of STOC 2019. 24–33. Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, and Rupak Majumdar. 2017. Model checking parameterized asynchronous shared-memory systems. Formal Methods Syst. Des. 50, 2-3 (2017), 140–167. https://doi.org/10.1007/s10703-016-0258-3 Paul Erdős and Richard Rado. 1952. Combinatorial Theorems on Classifications of Subsets of a Given Set. Proceedings of the London Mathematical Society s3-2, 1 (01 1952), 417–439. https://doi.org/10.1112/plms/s3-2.1.417 Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. 2016. Proving Liveness of Parameterized Programs. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016. ACM, 185–196. Alain Finkel and Philippe Schnoebelen. 2001. Well-structured transition systems everywhere! Theor. Comput. Sci. 256, 1-2 (2001), 63–92. Marie Fortin, Anca Muscholl, and Igor Walukiewicz. 2017. Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II (Lecture Notes in Computer Science), Vol. 10427. Springer, 155– 175. Pierre Ganty and Rupak Majumdar. 2012. Algorithmic verification of asynchronous programs. ACM Transactions on Programming Languages and Systems (TOPLAS) 34, 1 (2012), 6. Leonard H Haines. 1969. On free monoids partially ordered by embedding. Journal of Combinatorial Theory 6, 1 (1969), 94–98. David Harel. 1986. Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness. J. ACM 33 (1986), 224–248. Rodney R Howell, Louis E Rosier, and Hsu-Chun Yen. 1991. A taxonomy of fairness and temporal logic problems for Petri nets. Theoretical Computer Science 82, 2 (1991), 341–372. Petr Jančar. 1990. Decidability of a temporal logic problem for Petri nets. Theoretical Computer Science 74, 1 (1990), 71–93. Vineet Kahlon. 2008. Parameterization as Abstraction: A Tractable Approach to the Dataflow Analysis of Concurrent Programs. IEEE Computer Society, 181–192. Sambasiva Rao Kosaraju. 1982. Decidability of Reachability in Vector Addition Systems (Preliminary Version). In STOC ’82: Proc. of 14th ACM symp. on Theory of Computing. ACM, 267–281. Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, and Shaz Qadeer. 2020. Inductive sequentialization of asynchronous programs. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020. ACM, 227–242. Akash Lal and Thomas W. Reps. 2009. Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods in System Design 35, 1 (2009), 73–97. https://doi.org/10.1007/s10703-009-0078-9 Akash Lal, Tayssir Touili, Nicholas Kidd, and Thomas W. Reps. 2008. Interprocedural Analysis of Concurrent Programs Under a Context Bound. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings (Lecture Notes in Computer Science), Vol. 4963. Springer, 282–298. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. 2015. On the coverability problem for pushdown vector addition systems in one dimension. In ICALP 2015, Vol. 9135. 324–336. https://doi.org/10.1007/978-3-662-47666-6_26 Irina A. Lomazova and Philippe Schnoebelen. 1999. Some Decidability Results for Nested Petri Nets. In Perspectives of System Informatics, Third International Andrei Ershov Memorial Conference, PSI’99, Akademgorodok, Novosibirsk, Russia, July 6-9, 1999, Proceedings (Lecture Notes in Computer Science), Vol. 1755. Springer, 208–220. Ernst W. Mayr. 1981. An Algorithm for the General Petri Net Reachability Problem. In Proceedings of STOC 1981. 238–246. Anca Muscholl, Helmut Seidl, and Igor Walukiewicz. 2017. Reachability for Dynamic Parametric Processes. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings (Lecture Notes in Computer Science), Vol. 10145. Springer, 424–441. Madanlal Musuvathi and Shaz Qadeer. 2007. Iterative context bounding for systematic testing of multithreaded programs. In Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, PLDI 2007, San Diego, CA, USA, June 10-13, 2007. ACM, 446–455. Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. 2018. Reducing liveness to safety in first-order logic. Proc. ACM Program. Lang. 2, POPL (2018), 26:1–26:33. Rohit J. Parikh. 1966. On Context-Free Languages. J. ACM 13, 4 (1966), 570–581. Shaz Qadeer and Jakob Rehof. 2005. Context-Bounded Model Checking of Concurrent Software. In Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings (Lecture Notes in Computer Science), Vol. 3440. Springer, 93–107. Charles Rackoff. 1978. The covering and boundedness problems for vector addition systems. Theoretical Computer Science 6, 2 (1978), 223–231. Ganesan Ramalingam. 2000. Context-sensitive synchronization-sensitive analysis is undecidable. ACM TOPLAS 22(2) (2000), 416–430. Frank Plumpton Ramsey. 1930. On a Problem of Formal Logic. Proceedings of the London Mathematical Society s2-30, 1 (1930), 264–286. https://doi.org/10.1112/plms/s2-30.1.264 Salvatore La Torre, Margherita Napoli, and Gennaro Parlato. 2016. Scope-Bounded Pushdown Languages. Int. J. Found. Comput. Sci. 27, 2 (2016), 215–234. https://doi.org/10.1142/S0129054116400074 Moshe Y. Vardi. 1991. Verification of concurrent programs—the automata-theoretic framework. Annals of Pure and Applied Logic 51 (1991), 79–98. Kumar Neeraj Verma and Jean Goubault-Larrecq. 2005. Karp-Miller Trees for a Branching Extension of VASS. Discrete Mathematics & Theoretical Computer Science Vol. 7 (2005). Georg Zetzsche. 2013. Silent Transitions in Automata with Storage. (2013). arXiv:1302.3798 Full version of an article in Proceedings of ICALP 2013.

Context-Bounded Verification of Liveness: Conclusion, Acknowledgment & References

Unit testing is a fundamental practice in software development that ensures the reliability and correctness of your code. In this article, we will explore the key concepts of Java unit testing, including simple code examples, parametrization, exception testing, annotations such as , , , and , as well as the use of mocks and stubs. @Before @BeforeEach @After @AfterEach We'll also introduce the popular Mockito library for mocking and provide guidance on measuring code coverage using Maven plugins. The Importance of Unit Testing Unit testing is the practice of testing individual components or units of code in isolation to verify their correctness. The primary goal is to detect and fix bugs early in the development process, ensuring that each unit of code behaves as expected. Let's start by creating a simple calculator class that we can use for our examples. The class contains basic arithmetic operations: Calculator public class Calculator {
    public int add(int a, int b) {
        return a + b;
    }

    public int subtract(int a, int b) {
        return a - b;
    }

    public int multiply(int a, int b) {
        return a * b;
    }

    public int divide(int a, int b) {
        return a / b;
    }
} Writing a Simple Unit Test To create a unit test for our class, you can use the JUnit framework, a popular testing framework for Java. Let's write a simple unit test for the method: Calculator add import org.junit.jupiter.api.Test;
import static org.junit.jupiter.api.Assertions.assertEquals;

public class CalculatorTest {
    @Test
    public void testAdd() {
        Calculator calculator = new Calculator();
        int result = calculator.add(2, 3);
        assertEquals(5, result);
    }
} In this test, we import the necessary JUnit classes and annotate the test method with . We then create an instance of the class and assert that the result of the method is equal to the expected value (5). @Test Calculator add Parameterized Tests Parameterized tests allow you to run the same test logic with multiple sets of input data. This is useful for testing a method with various input values. To do this in JUnit, you can use the annotation and provide the input values and expected outcomes as parameters. Here's an example: @ParameterizedTest import org.junit.jupiter.params.ParameterizedTest;
import org.junit.jupiter.params.provider.CsvSource;
import static org.junit.jupiter.api.Assertions.assertEquals;

public class CalculatorTest {
    @ParameterizedTest
    @CsvSource({"2, 3, 5", "4, 7, 11", "0, 0, 0"})
    public void testAdd(int a, int b, int expected) {
        Calculator calculator = new Calculator();
        int result = calculator.add(a, b);
        assertEquals(expected, result);
    }
} In this example, the annotation allows us to provide multiple sets of input values and expected outcomes in a CSV format. The test method is executed for each combination, ensuring the correctness of the method. @ParameterizedTest add Exception Testing Testing exceptions is crucial to ensure your code handles errors appropriately. To test exception cases, you can use the annotation along with the method provided by JUnit. @Test assertThrows Here's an example: javaCopy codeimport org.junit.jupiter.api.Test;
import static org.junit.jupiter.api.Assertions.assertThrows;

public class CalculatorTest {
    @Test
    public void testDivideByZero() {
        Calculator calculator = new Calculator();
        assertThrows(ArithmeticException.class, () -> calculator.divide(5, 0));
    }
} In this test, we verify that dividing a number by zero in the class throws an . Calculator ArithmeticException Using Annotations: @Before, @BeforeEach, @After, and @AfterEach Annotations like , , , and are used to set up and tear down the test environment. These annotations help in managing common test initialization and cleanup tasks. @Before @BeforeEach @After @AfterEach and run once before and after all test methods in the test class, respectively. @Before @After and run before and after each test method. @BeforeEach @AfterEach Here's an example: import org.junit.jupiter.api.BeforeEach;
import org.junit.jupiter.api.AfterEach;
import org.junit.jupiter.api.Test;
import static org.junit.jupiter.api.Assertions.assertEquals;

public class CalculatorTest {
    private Calculator calculator;

    @BeforeEach
    public void setUp() {
        calculator = new Calculator();
    }

    @AfterEach
    public void tearDown() {
        calculator = null;
    }

    @Test
    public void testAdd() {
        int result = calculator.add(2, 3);
        assertEquals(5, result);
    }

    @Test
    public void testSubtract() {
        int result = calculator.subtract(5, 3);
        assertEquals(2, result);
    }
} In this example, the method is annotated with , and it initializes the object before each test. The method, annotated with , cleans up resources after each test. setUp @BeforeEach Calculator tearDown @AfterEach Mocks and Stubs Mocks and stubs are essential in unit testing when you want to isolate the code being tested from external dependencies, such as databases or web services. They allow you to simulate the behavior of these dependencies. A mock is an object that mimics the behavior of a real object but is under your control. It records interactions and allows you to verify that specific methods are called. Mock: A stub provides canned responses to method calls. It returns predefined data and is used to simulate certain behaviors of an external system. Stub: Let's expand the class to include a method that involves an external dependency and then create a stub to simulate that dependency. Calculator public class Calculator {
    private ExternalService externalService;

    public Calculator(ExternalService externalService) {
        this.externalService = externalService;
    }

    public int performComplexCalculation(int a, int b) {
        int result = externalService.multiply(a, b);
        return result + externalService.getConstant();
    }
} In this updated class, relies on an for multiplication and obtaining a constant value. Calculator performComplexCalculation ExternalService Here's how you might create a stub to test the class without depending on the actual . Calculator ExternalService import org.junit.jupiter.api.Test;

import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.mockito.Mockito.*;

public class CalculatorTest {
    @Test
    public void testPerformComplexCalculation() {
        // Create a stub for ExternalService
        ExternalService externalServiceStub = new ExternalService() {
            @Override
            public int multiply(int a, int b) {
                return a * b;
            }

            @Override
            public int getConstant() {
                return 5; // Stubbed constant value
            }
        };

        // Create the Calculator with the stubbed ExternalService
        Calculator calculator = new Calculator(externalServiceStub);

        // Test the performComplexCalculation method
        int result = calculator.performComplexCalculation(2, 3);
        assertEquals(11, result); // 2*3 + 5 (constant) = 11
    }
} In this test, is stubbed within the test method by creating an anonymous class that overrides the necessary methods. This way, the test method runs without depending on the actual implementation of . ExternalService Calculator ExternalService Stubs are useful for simulating the behavior of external systems or dependencies to isolate and test the specific functionality of a class or method. This allows you to control the behavior of the stub and focus on the unit under test without the need for actual external services. Introducing Mockito for Mocking Mockito is a popular Java library for creating and managing mock objects. Let's say we have a class that interacts with an external payment gateway. We can use Mockito to create a mock for the payment gateway: PaymentService import org.junit.jupiter.api.Test;
import static org.mockito.Mockito.*;

public class PaymentServiceTest {
    @Test
    public void testProcessPayment() {
        PaymentGateway paymentGateway = mock(PaymentGateway.class);
        PaymentService paymentService = new PaymentService(paymentGateway);

        when(paymentGateway.charge(100.0)).thenReturn(true);

        boolean result = paymentService.processPayment(100.0);

        assertTrue(result);
        verify(paymentGateway, times(1)).charge(100.0);
    }
} In this example, we create a mock and use the method to define its behavior. We then call the method on the class and verify that the method was called with the expected parameters. PaymentGateway when processPayment PaymentService charge Code Coverage and Maven Plugin Code coverage measures the percentage of code lines, branches, or statements that are executed by your unit tests. It helps you identify untested code and areas that may require additional testing. Maven is a popular build tool for Java projects, and you can integrate code coverage analysis into your Maven project using plugins like JaCoCo. Here's how to add JaCoCo to your project: Open your project's file. pom.xml Add the JaCoCo Maven plugin configuration: <build>
    <plugins>
        <plugin>
            <groupId>org.jacoco</groupId>
            <artifactId>jacoco-maven-plugin</artifactId>
            <version>0.8.7</version>
            <executions>
                <execution>
                    <goals>
                        <goal>prepare-agent</goal>
                    </goals>
                </execution>
                <execution>
                    <id>report</id>
                    <phase>test</phase>
                    <goals>
                        <goal>report</goal>
                    </goals>
                </execution>
            </executions>
        </plugin>
    </plugins>
</build> Run your Maven build with the following command: mvn clean verify After running the build, you can find the code coverage report in the file. This report provides detailed information about the coverage of your code by your unit tests. target/site/jacoco/index.html Conclusion Java unit testing is an essential practice for ensuring the reliability and correctness of your code. With tools like JUnit and Mockito, you can write effective unit tests and mocks for your components. By integrating code coverage analysis with Maven and JaCoCo, you can ensure that your tests cover a significant portion of your codebase. Regularly testing and maintaining unit tests will help you produce high-quality and robust Java applications. In the next part of this series, we will explore integration testing, a critical aspect of software testing that involves testing the interactions between different components and services to ensure the overall system functions correctly. Stay tuned for part two, where we will dive into the exciting world of integration testing!

Testing in Java: The Key Concepts [Part 1: Unit Testing]

জাভা পরীক্ষা: মূল ধারণা [পর্ব 1: ইউনিট পরীক্ষা]

Testen in Java: Die Schlüsselkonzepte [Teil 1: Unit-Tests]

Pruebas en Java: los conceptos clave [Parte 1: Pruebas unitarias]

Tests en Java : les concepts clés [Partie 1 : Tests unitaires]

जावा में परीक्षण: प्रमुख अवधारणाएँ [भाग 1: इकाई परीक्षण]

Java でのテスト: 主要な概念 [パート 1: 単体テスト]

Java 테스트: 주요 개념 [1부: 단위 테스트]

Teste em Java: os principais conceitos [Parte 1: Teste de unidade]

Тестирование на Java: ключевые понятия [Часть 1: Модульное тестирование]

Java'da Test Etme: Temel Kavramlar [Bölüm 1: Birim Testi]

Kiểm thử trong Java: Các khái niệm chính [Phần 1: Kiểm thử đơn vị]

Java 测试：关键概念 [第 1 部分：单元测试]

OpenAI is in a high-stakes legal battle with Elon Musk, who is suing the company to open source its groundbreaking AI models like GPT-4. While OpenAI may have the law on its side, I believe the ethical path forward is clear—it's time for the company to fully embrace the open-source ethos it was founded upon. As a former AI Specialist at OpenAI, I know OpenAI's stated mission has always been to ensure that artificial intelligence benefits all of humanity. The company's charter explicitly prioritizes this goal above generating financial returns. With the rapid rise of AI and the very real prospect of widespread job displacement, now is the time for OpenAI to double down on this mission through radical collaboration and transparency. Elon Musk helped found OpenAI precisely to keep advanced AI out of the exclusive control of a few tech giants or governments. The fear was that highly centralized, opaque AI development could lead to biased systems that disempower people and exacerbate inequality. Making frontier models like GPT-4 open source would accelerate innovation across the field and give everyone a stake in steering this transformative technology in a positive direction. Instead, OpenAI and its partner Microsoft now boast that “we are waiting for the competition to arrive. It will arrive, I’m sure, but the fact [is] that we have the … leading LLM out there.” Their most powerful models, including GPT-4, DALL-E, and now Sora, are all closed-source and gated. Entire countries like China and Russia are restricted from using OpenAI’s technologies. Accountability Through Openness Open-sourcing its models would also keep OpenAI honest and accountable. External researchers could audit the systems for hidden biases, safety issues, and potential misuse. The global AI ethics community could collaborate to make the models more inclusive and aligned with diverse human values. Perhaps even more importantly, the immense economic benefits of AI could be more evenly distributed if the core infrastructure is treated as a public good rather than the intellectual property of a few tech giants. While OpenAI has published research papers and shared some tools, it has stopped short of fully open-sourcing its most powerful models. Meanwhile, other prominent AI labs like H2O.ai have embraced a more open approach from the start. For instance, H2O recently released an open-source LLM called Danube-2, which can be downloaded in full from HuggingFace. Sri Ambati, CEO and founder of H2O.ai, said at H2O.ai’s GenAI World keynote that "AGI should be open source and in the public domain, at the service of humanity and the planet.” Even big tech players like Meta are exploring open-source AGI and giving outside researchers and the public more visibility into and agency over their AI work. OpenAI risks falling behind this trend and betraying its founding principles if it continues to treat its state-of-the-art models as proprietary secrets. The Business Case for Collaboration From a business standpoint, I understand the temptation for OpenAI to maintain exclusive control over its technology. But the history of the software industry shows that open source tends to win out in the long run through faster collaborative innovation and community support. Linux and the open-source movement conquered the once-dominant proprietary operating systems. Wikipedia displaced the traditional encyclopedia industry by crowdsourcing knowledge. With highly capable open source competitors to GPT-4 emerging, OpenAI's best path forward may be to focus on its expertise in scaling and commercializing a community-driven ecosystem rather than clinging to secrecy. Taking the High Road The transition to an open-source model would undoubtedly be challenging, but it's the right thing to do. OpenAI's leaders should return to their charter, reflect deeply on the kind of world they want to create, and take the bold path of openness and collaboration. Making advanced AI serve everyone is a historic challenge and opportunity. In the face of this technology's epochal impact on society, anything less than full transparency would be a dereliction of OpenAI's founding duty. I urge the company's leaders to resolve any legal disputes swiftly, open source their most important models, and help catalyze a global effort to develop AI as a public good. Democratizing access to AI is how we'll create the best outcomes for humanity. It's time for OpenAI to walk the walk of its open-source mission. OpenAI is in a high-stakes legal battle with Elon Musk, who is suing the company to open source its groundbreaking AI models like GPT-4. While OpenAI may have the law on its side , I believe the ethical path forward is clear—it's time for the company to fully embrace the open-source ethos it was founded upon. legal battle legal battle on its side on its side As a former AI Specialist at OpenAI, I know OpenAI's stated mission has always been to ensure that artificial intelligence benefits all of humanity. The company's charter explicitly prioritizes this goal above generating financial returns. With the rapid rise of AI and the very real prospect of widespread job displacement, now is the time for OpenAI to double down on this mission through radical collaboration and transparency. charter charter Elon Musk helped found OpenAI precisely to keep advanced AI out of the exclusive control of a few tech giants or governments. The fear was that highly centralized, opaque AI development could lead to biased systems that disempower people and exacerbate inequality. Making frontier models like GPT-4 open source would accelerate innovation across the field and give everyone a stake in steering this transformative technology in a positive direction. found OpenAI found OpenAI Instead, OpenAI and its partner Microsoft now boast that “we are waiting for the competition to arrive. It will arrive, I’m sure, but the fact [is] that we have the … leading LLM out there.” Their most powerful models, including GPT-4, DALL-E, and now Sora, are all closed-source and gated. Entire countries like China and Russia are restricted from using OpenAI’s technologies. boast boast restricted restricted Accountability Through Openness Open-sourcing its models would also keep OpenAI honest and accountable. External researchers could audit the systems for hidden biases, safety issues, and potential misuse. The global AI ethics community could collaborate to make the models more inclusive and aligned with diverse human values. Perhaps even more importantly, the immense economic benefits of AI could be more evenly distributed if the core infrastructure is treated as a public good rather than the intellectual property of a few tech giants. While OpenAI has published research papers and shared some tools, it has stopped short of fully open-sourcing its most powerful models. Meanwhile, other prominent AI labs like H2O.ai have embraced a more open approach from the start. For instance, H2O recently released an open-source LLM called Danube-2 , which can be downloaded in full from HuggingFace. Sri Ambati, CEO and founder of H2O.ai, said at H2O.ai’s GenAI World keynote that "AGI should be open source and in the public domain, at the service of humanity and the planet.” LLM called Danube-2 LLM called Danube-2 H2O.ai’s GenAI World keynote H2O.ai’s GenAI World keynote Even big tech players like Meta are exploring open-source AGI and giving outside researchers and the public more visibility into and agency over their AI work. OpenAI risks falling behind this trend and betraying its founding principles if it continues to treat its state-of-the-art models as proprietary secrets. open-source AGI open-source AGI The Business Case for Collaboration From a business standpoint, I understand the temptation for OpenAI to maintain exclusive control over its technology. But the history of the software industry shows that open source tends to win out in the long run through faster collaborative innovation and community support. win out in the long run win out in the long run Linux and the open-source movement conquered the once-dominant proprietary operating systems. Wikipedia displaced the traditional encyclopedia industry by crowdsourcing knowledge. With highly capable open source competitors to GPT-4 emerging, OpenAI's best path forward may be to focus on its expertise in scaling and commercializing a community-driven ecosystem rather than clinging to secrecy. Taking the High Road The transition to an open-source model would undoubtedly be challenging, but it's the right thing to do. OpenAI's leaders should return to their charter, reflect deeply on the kind of world they want to create, and take the bold path of openness and collaboration. Making advanced AI serve everyone is a historic challenge and opportunity. In the face of this technology's epochal impact on society, anything less than full transparency would be a dereliction of OpenAI's founding duty. I urge the company's leaders to resolve any legal disputes swiftly, open source their most important models, and help catalyze a global effort to develop AI as a public good. Democratizing access to AI is how we'll create the best outcomes for humanity. It's time for OpenAI to walk the walk of its open-source mission.

Why OpenAI Should Become Open-Source

This paper is available on arxiv under CC BY-SA 4.0 DEED license.
Authors:
(1) Lana L. Blaschke, Earth System Modelling, School of Engineering and Design, Technical University of Munich, Munich, Germany, Potsdam Institute for Climate Impact Research, Potsdam, Germany and lana.blaschke@pik-potsdam.de;
(2) Da Nian, Potsdam Institute for Climate Impact Research, Potsdam, Germany;
(3) Sebastian Bathiany,  Earth System Modelling, School of Engineering and Design, Technical University of Munich, Munich, Germany, and Potsdam Institute for Climate Impact Research, Potsdam, Germany;
(4)  Maya Ben-Yami,  Earth System Modelling, School of Engineering and Design, Technical University of Munich, Munich, Germany, and Potsdam Institute for Climate Impact Research, Potsdam, Germany;
(5) Taylor Smith, Institute of Geosciences, University of Potsdam, 14476 Potsdam, Germany;
(6)  Chris A. Boulton, Global Systems Institute, University of Exeter, EX4 4QE Exeter, UK ;
(7) Niklas Boers, Earth System Modelling, School of Engineering and Design, Technical University of Munich, Munich, Germany, Potsdam Institute for Climate Impact Research, Potsdam, Germany, Global Systems Institute, University of Exeter, EX4 4QE Exeter, UK, and Department of Mathematics, University of Exeter, EX4 4QF Exeter, UK. Table of Links Abstract and Introduction
Materials and Methods
Data
Results
Conclusions, Open Research Section and Conflict of Interest/Competing Interests
Author Contributions, Supplementary Information, Acknowledgments and References
Additional Insight from the Conceptual Model 
AMSR2 until 2022 Excluded Due to Missing Human Land Use Data
Investigation of Resilience Loss in AMSR2’s X-Band
Results Proving Robustness
Potential Driving Forces and Sources of Bias POTENTIAL DRIVING FORCES AND SOURCES OF BIAS Text S12. The influence of the South American Monsoon system as a potentially bistable system In the Amazon basin, the South American monsoon system and the atmospheric moisture recycling form a complex and potentially bi-stable system. Hence the monthly precipitation itself could exhibit signs of CSD, which would then drive vegetation changes that are wrongly interpreted as the destabilization of the vegetation. In Figure S16, the signs of the trend of variance, AC1 and spatial are compared between VOD and precipitation (Funk et al., 2014). We argue that due to the high amount of cells where the values differ in sign for the VIs and precipitation (sum of diagonal cells in boxes expected to be 50 % for random assignment), the observed changes in the indicators are likely a measure of critical slowing down in the vegetation and not only a direct effect of variability in precipitation. Text S13. The influence of changes in precipitation as a potential driving force If precipitation is the main driver of ARF resilience loss, one would expect that in regions with stronger decreases in precipitation (negative trend), more critical slowing down can be observed. This comparison in displayed in Figure S17. In parts, decreased precipitation could potentially explain the destabilization detected in the western Amazon basin by both bands of AMSR-E as well as in the western and northeastern regions detected by AMSR2’s bands. However it is important to note here that the number of cells with an increasing amount of precipitation and decreasing indicators and those with decreasing amount of precipitation and increasing indicators add up to only about 50 %, which is what is to be expected for a random assignment of positive and negative trends in both. Text S14. The influence of changes in temperature Instead of decreasing precipitation (see Figure S17, an increase in temperature can also lead to vegetation destabilization through water stress by higher evapo-transpirative demand. If this was the driver of the CSD, increasing temperatures must coincide with positive trends in the indicators of CSD in Figure S18. Yet changes in temperature cannot explain the detected destabilization in the years 2002 to 2011. For the time period of AMSR2, destabilization detected in the northeast (band C1) and the east (band C2) might at least partially be accounted for rising temperatures (the percentage of cells with rising/declining temperatures and in-/decreasing indicators falls between 48.6 % and up to 59.3 %). Text S15. The potential bias induced by saturation In case of optical sensors, their saturation over high biomass regions often renders the VIs insensitive to the subtle changes due to perturbations that a resilience analysis based on CSD relies on. The argument is that with decreasing biomass, the VIs become more sensitive, which then translates into a signal of CSD as a direct artifact of the higher perception of perturbations. Even though VOD results from observations of microwaves, we want to address the question of saturation in VOD. As Figure S19 shows, we cannot exclude this as an artifact for AMSRE’s band C as well as AMSR2’s two bands, as they hardly observed any cells with increasing biomass. Interestingly, AMSR-E’s band X detected an increase in biomass as well as a loss of resilience in most of the cells (77.3 % to 78.2 %). Thus, its signal of destabilization of almost the entire ARF during the years 2002 to 2011 is not an artifact of saturation of the band. This paper is available on arxiv under CC BY-SA 4.0 DEED license. Authors: (1) Lana L. Blaschke, Earth System Modelling, School of Engineering and Design, Technical University of Munich, Munich, Germany, Potsdam Institute for Climate Impact Research, Potsdam, Germany and lana.blaschke@pik-potsdam.de; (2) Da Nian, Potsdam Institute for Climate Impact Research, Potsdam, Germany; (3) Sebastian Bathiany,  Earth System Modelling, School of Engineering and Design, Technical University of Munich, Munich, Germany, and Potsdam Institute for Climate Impact Research, Potsdam, Germany; (4)  Maya Ben-Yami,  Earth System Modelling, School of Engineering and Design, Technical University of Munich, Munich, Germany, and Potsdam Institute for Climate Impact Research, Potsdam, Germany; (5) Taylor Smith, Institute of Geosciences, University of Potsdam, 14476 Potsdam, Germany; (6)  Chris A. Boulton, Global Systems Institute, University of Exeter, EX4 4QE Exeter, UK ; (7) Niklas Boers, Earth System Modelling, School of Engineering and Design, Technical University of Munich, Munich, Germany, Potsdam Institute for Climate Impact Research, Potsdam, Germany, Global Systems Institute, University of Exeter, EX4 4QE Exeter, UK, and Department of Mathematics, University of Exeter, EX4 4QF Exeter, UK. This paper is available on arxiv under CC BY-SA 4.0 DEED license. Authors: Authors: (1) Lana L. Blaschke, Earth System Modelling, School of Engineering and Design, Technical University of Munich, Munich, Germany, Potsdam Institute for Climate Impact Research, Potsdam, Germany and lana.blaschke@pik-potsdam.de; (2) Da Nian, Potsdam Institute for Climate Impact Research, Potsdam, Germany; (3) Sebastian Bathiany,  Earth System Modelling, School of Engineering and Design, Technical University of Munich, Munich, Germany, and Potsdam Institute for Climate Impact Research, Potsdam, Germany; (4)  Maya Ben-Yami,  Earth System Modelling, School of Engineering and Design, Technical University of Munich, Munich, Germany, and Potsdam Institute for Climate Impact Research, Potsdam, Germany; (5) Taylor Smith, Institute of Geosciences, University of Potsdam, 14476 Potsdam, Germany; (6)  Chris A. Boulton, Global Systems Institute, University of Exeter, EX4 4QE Exeter, UK ; (7) Niklas Boers, Earth System Modelling, School of Engineering and Design, Technical University of Munich, Munich, Germany, Potsdam Institute for Climate Impact Research, Potsdam, Germany, Global Systems Institute, University of Exeter, EX4 4QE Exeter, UK, and Department of Mathematics, University of Exeter, EX4 4QF Exeter, UK. Table of Links Abstract and Introduction Materials and Methods Data Results Conclusions, Open Research Section and Conflict of Interest/Competing Interests Author Contributions, Supplementary Information, Acknowledgments and References Additional Insight from the Conceptual Model AMSR2 until 2022 Excluded Due to Missing Human Land Use Data Investigation of Resilience Loss in AMSR2’s X-Band Results Proving Robustness Potential Driving Forces and Sources of Bias Abstract and Introduction Abstract and Introduction Materials and Methods Materials and Methods Data Data Results Results Conclusions, Open Research Section and Conflict of Interest/Competing Interests Conclusions, Open Research Section and Conflict of Interest/Competing Interests Author Contributions, Supplementary Information, Acknowledgments and References Author Contributions, Supplementary Information, Acknowledgments and References Additional Insight from the Conceptual Model Additional Insight from the Conceptual Model AMSR2 until 2022 Excluded Due to Missing Human Land Use Data AMSR2 until 2022 Excluded Due to Missing Human Land Use Data Investigation of Resilience Loss in AMSR2’s X-Band Investigation of Resilience Loss in AMSR2’s X-Band Results Proving Robustness Results Proving Robustness Potential Driving Forces and Sources of Bias Potential Driving Forces and Sources of Bias POTENTIAL DRIVING FORCES AND SOURCES OF BIAS Text S12. The influence of the South American Monsoon system as a potentially bistable system In the Amazon basin, the South American monsoon system and the atmospheric moisture recycling form a complex and potentially bi-stable system. Hence the monthly precipitation itself could exhibit signs of CSD, which would then drive vegetation changes that are wrongly interpreted as the destabilization of the vegetation. In Figure S16, the signs of the trend of variance, AC1 and spatial are compared between VOD and precipitation (Funk et al., 2014). We argue that due to the high amount of cells where the values differ in sign for the VIs and precipitation (sum of diagonal cells in boxes expected to be 50 % for random assignment), the observed changes in the indicators are likely a measure of critical slowing down in the vegetation and not only a direct effect of variability in precipitation. Text S13. The influence of changes in precipitation as a potential driving force If precipitation is the main driver of ARF resilience loss, one would expect that in regions with stronger decreases in precipitation (negative trend), more critical slowing down can be observed. This comparison in displayed in Figure S17. In parts, decreased precipitation could potentially explain the destabilization detected in the western Amazon basin by both bands of AMSR-E as well as in the western and northeastern regions detected by AMSR2’s bands. However it is important to note here that the number of cells with an increasing amount of precipitation and decreasing indicators and those with decreasing amount of precipitation and increasing indicators add up to only about 50 %, which is what is to be expected for a random assignment of positive and negative trends in both. Text S14. The influence of changes in temperature Instead of decreasing precipitation (see Figure S17, an increase in temperature can also lead to vegetation destabilization through water stress by higher evapo-transpirative demand. If this was the driver of the CSD, increasing temperatures must coincide with positive trends in the indicators of CSD in Figure S18. Yet changes in temperature cannot explain the detected destabilization in the years 2002 to 2011. For the time period of AMSR2, destabilization detected in the northeast (band C1) and the east (band C2) might at least partially be accounted for rising temperatures (the percentage of cells with rising/declining temperatures and in-/decreasing indicators falls between 48.6 % and up to 59.3 %). Text S15. The potential bias induced by saturation In case of optical sensors, their saturation over high biomass regions often renders the VIs insensitive to the subtle changes due to perturbations that a resilience analysis based on CSD relies on. The argument is that with decreasing biomass, the VIs become more sensitive, which then translates into a signal of CSD as a direct artifact of the higher perception of perturbations. Even though VOD results from observations of microwaves, we want to address the question of saturation in VOD. As Figure S19 shows, we cannot exclude this as an artifact for AMSRE’s band C as well as AMSR2’s two bands, as they hardly observed any cells with increasing biomass. Interestingly, AMSR-E’s band X detected an increase in biomass as well as a loss of resilience in most of the cells (77.3 % to 78.2 %). Thus, its signal of destabilization of almost the entire ARF during the years 2002 to 2011 is not an artifact of saturation of the band.

Loss of Amazon Rainforest Resilience: Potential Driving Forces and Sources of Bias

AI-Powered Localization Using an Open-source Project as a Case Study

Let's build a chatbot with just Python using the Streamlit library, Ollama, and Microsoft Phi-3. Streamlit Streamlit turns data scripts into shareable web apps in minutes. All in pure Python. No front‑end experience required. You can find more info in the official Streamlit docs. Ollama Ollama allows you to run open-source large language models, locally. You can find more info in the official Ollama docs. Phi-3 Mini Phi-3 Mini is a 3.8B parameters, lightweight, state-of-the-art open model by Microsoft. You can find more info in the official Phi-3 Mini docs. Steps Create a new conda environment conda create --name envStreamPhi Activate the environment conda activate envStreamPhi Install ollama Download Ollama from https://ollama.com/download pull the phi-3 model The model we will be using is located here: ollama pull phi3 Pull the Embeddings model: ollama pull nomic-embed-text Test installation streamlit hello Build the AI Assistant In order to build the AI assistant, you have 2 choices: clone the repo and get all the code from the get-go, or code along with me. I - First option: Clone the project from GitHub git clone https://github.com/JalelTounsi/oLLaMaStreamPhi.git Run the Application streamlit run app.py II - Second Option: Code Along Create your app.py file Add Imports import streamlit as st
import ollama Add the Defacto Message if "messages" not in st.session_state:
    st.session_state["messages"] = [{"role": "assistant", "content": "Hello tehre, how can I help you, today?"}] Add the Message History for msg in st.session_state.messages:
    if msg["role"] == "user":
        st.chat_message(msg["role"], avatar="🧑‍💻").write(msg["content"])
    else:
        st.chat_message(msg["role"], avatar="🤖").write(msg["content"]) Configure Model def generate_response():
    response = ollama.chat(model='phi3', stream=True, messages=st.session_state.messages)
    for partial_resp in response:
        token = partial_resp["message"]["content"]
        st.session_state["full_message"] += token
        yield token Configure the Prompt if prompt := st.chat_input():
    st.session_state.messages.append({"role": "user", "content": prompt})
    st.chat_message("user", avatar="🧑‍💻").write(prompt)
    st.session_state["full_message"] = ""
    st.chat_message("assistant", avatar="🤖").write_stream(generate_response)
    st.session_state.messages.append({"role": "assistant", "content": st.session_state["full_message"]}) All the Codebase of app.py import streamlit as st
import ollama

st.title("💬 Phi3 Chatbot")

if "messages" not in st.session_state:
    st.session_state["messages"] = [{"role": "assistant", "content": "Hello tehre, how can I help you, today?"}]

### Write Message History
for msg in st.session_state.messages:
    if msg["role"] == "user":
        st.chat_message(msg["role"], avatar="🧑‍💻").write(msg["content"])
    else:
        st.chat_message(msg["role"], avatar="🤖").write(msg["content"])

## Configure the model
def generate_response():
    response = ollama.chat(model='phi3', stream=True, messages=st.session_state.messages)
    for partial_resp in response:
        token = partial_resp["message"]["content"]
        st.session_state["full_message"] += token
        yield token

if prompt := st.chat_input():
    st.session_state.messages.append({"role": "user", "content": prompt})
    st.chat_message("user", avatar="🧑‍💻").write(prompt)
    st.session_state["full_message"] = ""
    st.chat_message("assistant", avatar="🤖").write_stream(generate_response)
    st.session_state.messages.append({"role": "assistant", "content": st.session_state["full_message"]}) Run the Streamlit App streamlit run app.py Bonus Point Feel free to check this video to understand the code, follow along, and run the AI assistant locally on your computer: AI assistant using Streamlit, Phi3, and Ollama Let's build a chatbot with just Python using the Streamlit library, Ollama , and Microsoft Phi-3 . Streamlit Ollama Microsoft Phi-3 Streamlit Streamlit turns data scripts into shareable web apps in minutes. All in pure Python. No front‑end experience required. You can find more info in the official Streamlit docs . official Streamlit docs Ollama Ollama allows you to run open-source large language models, locally. You can find more info in the official Ollama docs . official Ollama Ollama docs Phi-3 Mini Phi-3 Mini is a 3.8B parameters, lightweight, state-of-the-art open model by Microsoft. You can find more info in the official Phi-3 Mini docs . Phi-3 Mini Phi-3 Mini docs Steps Create a new conda environment conda create --name envStreamPhi conda create --name envStreamPhi Activate the environment conda activate envStreamPhi conda activate envStreamPhi Install ollama Download Ollama from https://ollama.com/download https://ollama.com/download pull the phi-3 model The model we will be using is located here : here ollama pull phi3 ollama pull phi3 Pull the Embeddings model: ollama pull nomic-embed-text ollama pull nomic-embed-text Test installation streamlit hello streamlit hello Build the AI Assistant In order to build the AI assistant, you have 2 choices: clone the repo and get all the code from the get-go, or code along with me. I - First option: Clone the project from GitHub git clone https://github.com/JalelTounsi/oLLaMaStreamPhi.git git clone https://github.com/JalelTounsi/oLLaMaStreamPhi.git Run the Application streamlit run app.py streamlit run app.py II - Second Option: Code Along Create your app.py file app.py Add Imports import streamlit as st
import ollama import streamlit as st
import ollama Add the Defacto Message if "messages" not in st.session_state:
    st.session_state["messages"] = [{"role": "assistant", "content": "Hello tehre, how can I help you, today?"}] if "messages" not in st.session_state:
    st.session_state["messages"] = [{"role": "assistant", "content": "Hello tehre, how can I help you, today?"}] Add the Message History for msg in st.session_state.messages:
    if msg["role"] == "user":
        st.chat_message(msg["role"], avatar="🧑‍💻").write(msg["content"])
    else:
        st.chat_message(msg["role"], avatar="🤖").write(msg["content"]) for msg in st.session_state.messages:
    if msg["role"] == "user":
        st.chat_message(msg["role"], avatar="🧑‍💻").write(msg["content"])
    else:
        st.chat_message(msg["role"], avatar="🤖").write(msg["content"]) Configure Model def generate_response():
    response = ollama.chat(model='phi3', stream=True, messages=st.session_state.messages)
    for partial_resp in response:
        token = partial_resp["message"]["content"]
        st.session_state["full_message"] += token
        yield token def generate_response():
    response = ollama.chat(model='phi3', stream=True, messages=st.session_state.messages)
    for partial_resp in response:
        token = partial_resp["message"]["content"]
        st.session_state["full_message"] += token
        yield token Configure the Prompt if prompt := st.chat_input():
    st.session_state.messages.append({"role": "user", "content": prompt})
    st.chat_message("user", avatar="🧑‍💻").write(prompt)
    st.session_state["full_message"] = ""
    st.chat_message("assistant", avatar="🤖").write_stream(generate_response)
    st.session_state.messages.append({"role": "assistant", "content": st.session_state["full_message"]}) if prompt := st.chat_input():
    st.session_state.messages.append({"role": "user", "content": prompt})
    st.chat_message("user", avatar="🧑‍💻").write(prompt)
    st.session_state["full_message"] = ""
    st.chat_message("assistant", avatar="🤖").write_stream(generate_response)
    st.session_state.messages.append({"role": "assistant", "content": st.session_state["full_message"]}) All the Codebase of app.py app.py import streamlit as st
import ollama

st.title("💬 Phi3 Chatbot")

if "messages" not in st.session_state:
    st.session_state["messages"] = [{"role": "assistant", "content": "Hello tehre, how can I help you, today?"}]

### Write Message History
for msg in st.session_state.messages:
    if msg["role"] == "user":
        st.chat_message(msg["role"], avatar="🧑‍💻").write(msg["content"])
    else:
        st.chat_message(msg["role"], avatar="🤖").write(msg["content"])

## Configure the model
def generate_response():
    response = ollama.chat(model='phi3', stream=True, messages=st.session_state.messages)
    for partial_resp in response:
        token = partial_resp["message"]["content"]
        st.session_state["full_message"] += token
        yield token

if prompt := st.chat_input():
    st.session_state.messages.append({"role": "user", "content": prompt})
    st.chat_message("user", avatar="🧑‍💻").write(prompt)
    st.session_state["full_message"] = ""
    st.chat_message("assistant", avatar="🤖").write_stream(generate_response)
    st.session_state.messages.append({"role": "assistant", "content": st.session_state["full_message"]}) import streamlit as st
import ollama

st.title("💬 Phi3 Chatbot")

if "messages" not in st.session_state:
    st.session_state["messages"] = [{"role": "assistant", "content": "Hello tehre, how can I help you, today?"}]

### Write Message History
for msg in st.session_state.messages:
    if msg["role"] == "user":
        st.chat_message(msg["role"], avatar="🧑‍💻").write(msg["content"])
    else:
        st.chat_message(msg["role"], avatar="🤖").write(msg["content"])

## Configure the model
def generate_response():
    response = ollama.chat(model='phi3', stream=True, messages=st.session_state.messages)
    for partial_resp in response:
        token = partial_resp["message"]["content"]
        st.session_state["full_message"] += token
        yield token

if prompt := st.chat_input():
    st.session_state.messages.append({"role": "user", "content": prompt})
    st.chat_message("user", avatar="🧑‍💻").write(prompt)
    st.session_state["full_message"] = ""
    st.chat_message("assistant", avatar="🤖").write_stream(generate_response)
    st.session_state.messages.append({"role": "assistant", "content": st.session_state["full_message"]}) Run the Streamlit App streamlit run app.py streamlit run app.py Bonus Point Feel free to check this video to understand the code, follow along, and run the AI assistant locally on your computer: AI assistant using Streamlit, Phi3, and Ollama AI assistant using Streamlit, Phi3, and Ollama

CYSOURCE

cysrc.com

-- employees

Since n.d.

COMPANY RANKING

CYSOURCE

EVERGREEN INDEX #3086

CYSOURCE WIKI

Apply to get your Tech Company News Page live on HackerNoon.com today!

CYSOURCE

cysrc.com

-- employees

Since n.d.

COMPANY RANKING

CYSOURCE

EVERGREEN INDEX #3086

RELATED COMPANIESRANK

STORIES ABOUT CYSOURCE

CYSOURCE WIKI

Apply to get your Tech Company News Page live on HackerNoon.com today!